New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > syl5eq | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5eq.1 | |
syl5eq.2 |
Ref | Expression |
---|---|
syl5eq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5eq.1 | . . 3 | |
2 | 1 | a1i 10 | . 2 |
3 | syl5eq.2 | . 2 | |
4 | 2, 3 | eqtrd 2385 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 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-ex 1542 df-cleq 2346 |
This theorem is referenced by: syl5req 2398 syl5eqr 2399 3eqtr3a 2409 3eqtr4g 2410 csbtt 3148 csbvarg 3163 csbie2g 3182 rabbi2dva 3463 disjssun 3608 difprsn2 3848 difsnid 3854 intsng 3961 riinn0 4040 iinxsng 4042 rintn0 4056 prprc2 4122 prprc1 4123 pw1eqadj 4332 iotaval 4350 iotanul 4354 nnsucelrlem4 4427 ssfin 4470 dmxp 4923 resabs1 4992 resabs2 4993 resopab2 5001 resiima 5012 imasn 5018 ndmima 5025 xpdisj1 5047 xpdisj2 5048 resdisj 5050 rnxp 5051 dfco2a 5081 cores2 5091 fnun 5189 fnresdisj 5193 fnima 5201 f1orescnv 5301 resdif 5306 f1ococnv2 5309 fvprc 5325 tz6.12-1 5344 tz6.12-2 5346 fnrnfv 5364 fvun 5378 fvun2 5380 ressnop0 5436 fvunsn 5444 fvsnun2 5448 fvpr1 5449 funiunfv 5467 f1oiso2 5500 resoprab2 5582 fnoprabg 5585 ovidig 5593 ov6g 5600 ovconst2 5611 ndmovg 5613 ndmovcl 5614 ndmov 5615 caovmo 5645 elovex12 5648 fvmptnf 5723 fntxp 5804 fnpprod 5843 map0b 6024 enpw1 6062 sbthlem1 6203 dflec2 6210 nchoicelem7 6295 |
Copyright terms: Public domain | W3C validator |