New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sylan9eq | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
sylan9eq.1 | |
sylan9eq.2 |
Ref | Expression |
---|---|
sylan9eq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9eq.1 | . 2 | |
2 | sylan9eq.2 | . 2 | |
3 | eqtr 2370 | . 2 | |
4 | 1, 2, 3 | syl2an 463 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 wceq 1642 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-cleq 2346 |
This theorem is referenced by: sylan9req 2406 sylan9eqr 2407 nineq12 3236 symdifeq12 3250 difeq12 3380 uneq12 3413 ineq12 3452 ifeq12 3675 ifbi 3679 preq12 3801 opkeq12 4061 preq12b 4127 xpkeq12 4200 addceq12 4385 opeq12 4580 xpeq12 4803 nfimad 4954 funimass1 5169 f1orescnv 5301 resdif 5306 oveq12 5532 caovmo 5645 cbvmpt2v 5680 fvmpt2 5704 ovmpt2g 5715 fvmptnf 5723 map0 6025 enmap2lem5 6067 enmap1lem3 6071 enmap1lem5 6073 |
Copyright terms: Public domain | W3C validator |