Clicking on the inference rule ID selects that inference rule for the step

name	latex	input count	feed count	output count
LHS of expr 1 equals LHS of expr 2	LHS of Eq.~ ef{eq:#1} is equal to LHS of Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	2	0	1
RHS of expr 1 equals RHS of expr 2	RHS of Eq.~ ef{eq:#1} is equal to RHS of Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	2	0	1
X cross both sides by	Take cross product of $#1$ and Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
X dot both sides	Take inner product of $#1$ with Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
add X to both sides	Add $#1$ to both sides of Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
add expr 1 to expr 2	Add Eq.~ ef{eq:#1} to Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#2}.	2	0	1
add zero to LHS	Add zero to LHS of Eq.~ ef{eq:#2}, where $0=#1$; yields Eq.~ ef{eq:#3}.	1	1	1
add zero to RHS	Add zero to RHS of Eq.~ ef{eq:#2}, where $0=#1$; yields Eq.~ ef{eq:#3}.	1	1	1
apply divergence	Apply divergence to both sides of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
apply function to both sides of expression	Apply function $#1$ with argument $#2$ to Eq.~ ef{eq:#3}; yields Eq.~ ef{eq:#4}	1	2	1
apply gradient to scalar function	Apply gradient to both sides of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
apply operator to bra	Apply operator in Eq.~ ef{eq:#1} to bra; yields Eq.~ ef{eq:#2}.	1	0	1
apply operator to ket	Apply operator in Eq.~ ef{eq:#1} to ket; yields Eq.~ ef{eq:#2}.	1	0	1
assume N dimensions	Assume $#1$ dimensions; decompose vector to be Eq.~ ef{eq:#2}.	0	1	1
both sides cross X	Take cross product of Eq.~ ef{eq:#2} and $#1$; yields Eq.~ ef{eq:#3}	1	1	1
both sides dot X	Take inner product of Eq.~ ef{eq:#2} with $#1$; yields Eq.~ ef{eq:#3}	1	1	1
boundary condition	Boundary condition: Eq.~ ef{eq:#2} when Eq.~ ef{eq#1}.	1	0	1
boundary condition for expression	A boundary condition for Eq.~ ef{eq:#1} is Eq.~ ef{eq:#2}	1	0	1
change five variables in expression	Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ and $#9$ to $#10$ in Eq.~ ef{eq:#11}; yields Eq.~ ef{eq:#12}.	1	10	1
change four variables in expression	Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ in Eq.~ ef{eq:#9}; yields Eq.~ ef{eq:#10}.	1	8	1
change six variables in expression	Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ and $#9$ to $#10$ and $#11$ to $#12$ in Eq.~ ef{eq:#13}; yields Eq.~ ef{eq:#14}.	1	12	1
change three variables in expression	Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ in Eq.~ ef{eq:#7}; yields Eq.~ ef{eq:#8}.	1	6	1
change two variables in expression	Change variable $#1$ to $#2$ and $#3$ to $#4$ in Eq.~ ef{eq:#5}; yields Eq.~ ef{eq:#6}.	1	4	1
change variable X to Y	Change variable $#1$ to $#2$ in Eq.~ ef{eq:#3}; yields Eq.~ ef{eq:#4}.	1	2	1
claim LHS equals RHS	Thus we see that LHS of Eq.~ ef{eq:#1} is equal to RHS.	1	0	0
claim expr 1 equals expr 2	Thus we see that Eq.~ ef{eq:#1} is equivalent to Eq.~ ef{eq:#2}.	2	0	0
combine like terms	Combine like terms in Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
conjugate both sides	Conjugate both sides of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
conjugate function X	Conjugate $#1$ in Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
conjugate transpose both sides	Conjugate transpose of both sides of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
declare assumption	Eq.~ ef{eq:#1} is an assumption.	0	0	1
declare final expression	Eq.~ ef{eq:#1} is one of the final equations.	1	0	0
declare guess solution	Judicious choice as a guessed solution to Eq.~ ef{eq:#1} is Eq.~ ef{eq:#2},	1	0	1
declare identity	Eq.~ ef{eq:#1} is an identity.	0	0	1
declare initial expression	Eq.~ ef{eq:#1} is an initial equation.	0	0	1
differentiate with respect to	Differentiate Eq.~ ef{eq:#2} with respect to $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
distribute conjugate to factors	Distribute conjugate to factors in Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
distribute conjugate transpose to factors	Distribute conjugate transpose to factors in Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
divide both sides by	Divide both sides of Eq.~ ef{eq:#2} by $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
divide expr 1 by expr 2	Divide Eq.~ ef{eq:#1} by Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	2	0	1
drop non-dominant term	Based on the assumption $#1$, drop non-dominant term in Eq.~ ef{#2}; yeilds Eq.~ ef{#3}	1	1	1
evaluate definite integral	Evaluate definite integral Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
expand LHS	Expand the LHS of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
expand RHS	Expand the RHS of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
expand integrand	Expand integrand of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
expand magnitude to conjugate	Expand $#1$ in Eq.~ ef{eq:#2} with conjugate; yields Eq.~ ef{eq:#3}.	1	1	1
expr 1 is equivalent to expr 2 under the condition	Eq.~ ef{eq:#1} is equivalent to Eq.~ ef{eq:#2} under the condition in Eq.~ ef{eq:#3}.	2	0	1
expr 1 is true under condition expr 2	Eq.~ ef{eq:#1} is valid when Eq.~ ef{eq:#2} occurs; yields Eq.~ ef{eq:#3}.	2	0	1
factor out X	Factor $#1$ from Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
factor out X from LHS	Factor $#1$ from the LHS of Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
factor out X from RHS	Factor $#1$ from the RHS of Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
function is even	$#1$ is even with respect to $#2$, so replace $#1$ with $#3$ in Eq.~ ef{eq:#4}; yields Eq.~ ef{eq:#5}.	1	3	1
function is odd	$#1$ is odd with respect to $#2$, so replace $#1$ with $#3$ in Eq.~ ef{eq:#4}; yields Eq.~ ef{eq:#5}.	1	3	1
indefinite integral over	Indefinite integral of both sides of Eq.~ ef{eq:#2} over $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
indefinite integrate LHS over	Indefinite integral of LHS of Eq.~ ef{eq:#2} over $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
indefinite integrate RHS over	Indefinite integral of RHS of Eq.~ ef{eq:#2} over $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
indefinite integration	Indefinite integral of both sides of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
integrate	Integrate Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}.	1	0	1
integrate over from to	Integrate Eq.~ ef{eq:#4} over $#1$ from lower limit $#2$ to upper limit $#3$; yields Eq.~ ef{eq:#5}.	1	3	1
make expr power	Make Eq.~ ef{eq:#2} the power of $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
maximum of expression	The maximum of Eq.~ ef{eq:#2} with respect to $#1$ is Eq.~ ef{eq:#3}	1	1	1
multiply LHS by unity	Multiply LHS of Eq.~ ef{eq:#2} by 1, which in this case is $#1$; yields Eq.~ ef{eq:#3}	1	1	1
multiply RHS by unity	Multiply RHS of Eq.~ ef{eq:#2} by 1, which in this case is $#1$; yields Eq.~ ef{eq:#3}	1	1	1
multiply both sides by	Multiply both sides of Eq.~ ef{eq:#2} by $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
multiply expr 1 by expr 2	Multiply Eq.~ ef{eq:#1} by Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	2	0	1
normalization condition	Normalization condition is Eq.~ ef{eq:#1}.	0	0	1
partially differentiate with respect to	Partially differentiate Eq.~ ef{eq:#2} with respect to $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
raise both sides to power	Raise both sides of Eq.~ ef{eq:#2} to $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
replace constant with value	Replace constant $#1$ with value $#2$ and units $#3$ in Eq.~ ef{eq:#4}; yields Eq.~ ef{eq:#5}	1	3	1
replace curl with LeviCevita summation contravariant	Replace curl in Eq.~ ef{eq:#1} with Levi-Cevita contravariant; yields Eq.~ ef{eq:#2}.	1	0	1
replace scalar with vector	Replace scalar variables in Eq.~ ef{eq:#1} with equivalent vector variables; yields Eq.~ ef{eq:#2}.	1	0	1
replace summation notation with vector notation	Replace summation notation in Eq.~ ef{eq:#1} with vector notation; yields Eq.~ ef{eq:#2}.	1	0	1
select imaginary parts	Select imaginary parts of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
select real parts	Select real parts of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
separate three vector components	Separate three vector components in Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2} and Eq.~ ef{eq:#3} and Eq.~ ef{eq:#4}.	1	0	3
separate two vector components	Separate two vector components in Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2} and Eq.~ ef{eq:#3}	1	0	2
separate vector into two trigonometric ratios	Separate vector in Eq.~ ef{eq:#2} into components related by angle $#1$; yields Eq.~ ef{eq:#3} and Eq.~ ef{eq:#4}.	1	1	2
simplify	Simplify Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
solve for X	Solve Eq.~ ef{eq:#2} for $#1$; yields Eq.~ ef{eq:#3}.	1	1	1
square root both sides	Take the square root of both sides of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2} and Eq.~ ef{eq:#3}.	1	0	2
substitute LHS of expr 1 into expr 2	Substitute LHS of Eq.~ ef{eq:#1} into Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	2	0	1
substitute LHS of five expressions into expression	Substitute LHS of Eq.~ ef{eq:#1} and LHS of Eq.~ ef{eq:#2} and LHS of Eq.~ ef{eq:#3} and LHS of Eq.~ ef{eq:#4} and LHS of Eq.~ ef{eq:#5} into Eq.~ ef{eq:#6}; yields Eq.~ ef{eq:#7}.	6	0	1
substitute LHS of four expressions into expression	Substitute LHS of Eq.~ ef{eq:#1} and LHS of Eq.~ ef{eq:#2} and LHS of Eq.~ ef{eq:#3} and LHS of Eq.~ ef{eq:#4} into Eq.~ ef{eq:#5}; yields Eq.~ ef{eq:#6}.	5	0	1
substitute LHS of six expressions into expression	Substitute LHS of Eq.~ ef{eq:#1} and LHS of Eq.~ ef{eq:#2} and LHS of Eq.~ ef{eq:#3} and LHS of Eq.~ ef{eq:#4} and LHS of Eq.~ ef{eq:#5} and LHS of Eq.~ ef{eq:#6} into Eq.~ ef{eq:#7}; yields Eq.~ ef{eq:#8}.	7	0	1
substitute LHS of three expressions into expression	Substitute LHS of Eq.~ ef{eq:#1} and LHS of Eq.~ ef{eq:#2} and LHS of Eq.~ ef{eq:#3} into Eq.~ ef{eq:#4}; yields Eq.~ ef{eq:#5}.	4	0	1
substitute LHS of two expressions into expression	Substitute LHS of Eq.~ ef{eq:#1} and LHS of Eq.~ ef{eq:#2} into Eq.~ ef{eq:#3}; yields Eq.~ ef{eq:#4}.	3	0	1
substitute RHS of expr 1 into expr 2	Substitute RHS of Eq.~ ef{eq:#1} into Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	2	0	1
subtract X from both sides	Subtract $#1$ from both sides of Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#3}.	1	1	1
subtract expr 1 from expr 2	Subtract Eq.~ ef{eq:#1} from Eq.~ ef{eq:#2}; yields Eq.~ ef{eq:#2}.	2	0	1
sum exponents	Sum exponents on LHS and RHS of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
sum exponents LHS	Sum exponents on LHS of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
sum exponents RHS	Sum exponents on RHS of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1
swap LHS with RHS	Swap LHS of Eq.~ ef{eq:#1} with RHS; yields Eq.~ ef{eq:#2}.	1	0	1
take curl of both sides	Apply curl to both sides of Eq.~ ef{eq:#1}; yields Eq.~ ef{eq:#2}.	1	0	1

The next step is to associate the inference rule with expressions. The expressions have to already exist in the database.

If you don't see the inference rule you need,
Create a new inference rule