Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqtr2di | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
eqtr2di.1 | |
eqtr2di.2 |
Ref | Expression |
---|---|
eqtr2di |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr2di.1 | . . 3 | |
2 | eqtr2di.2 | . . 3 | |
3 | 1, 2 | eqtrdi 2213 | . 2 |
4 | 3 | eqcomd 2170 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: eqtr4id 2216 elxp4 5085 elxp5 5086 fo1stresm 6121 fo2ndresm 6122 eloprabi 6156 fo2ndf 6186 xpsnen 6778 xpassen 6787 ac6sfi 6855 undifdc 6880 ine0 8283 nn0n0n1ge2 9252 fzval2 9938 fseq1p1m1 10019 fsum2dlemstep 11361 modfsummodlemstep 11384 fprod2dlemstep 11549 ef4p 11621 sin01bnd 11684 odd2np1 11795 sqpweven 12086 2sqpwodd 12087 psmetdmdm 12871 xmetdmdm 12903 dveflem 13234 reeff1oleme 13240 abssinper 13314 |
Copyright terms: Public domain | W3C validator |