Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6req | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
syl6req.1 | |
syl6req.2 |
Ref | Expression |
---|---|
syl6req |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6req.1 | . . 3 | |
2 | syl6req.2 | . . 3 | |
3 | 1, 2 | syl6eq 2166 | . 2 |
4 | 3 | eqcomd 2123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: syl6reqr 2169 elxp4 4996 elxp5 4997 fo1stresm 6027 fo2ndresm 6028 eloprabi 6062 fo2ndf 6092 xpsnen 6683 xpassen 6692 ac6sfi 6760 undifdc 6780 ine0 8124 nn0n0n1ge2 9089 fzval2 9761 fseq1p1m1 9842 fsum2dlemstep 11171 modfsummodlemstep 11194 ef4p 11327 sin01bnd 11391 odd2np1 11497 sqpweven 11780 2sqpwodd 11781 psmetdmdm 12420 xmetdmdm 12452 dveflem 12782 abssinper 12854 |
Copyright terms: Public domain | W3C validator |