![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > eqtrd | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtrd.1 | ⊢ (φ → A = B) |
eqtrd.2 | ⊢ (φ → B = C) |
Ref | Expression |
---|---|
eqtrd | ⊢ (φ → A = C) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtrd.1 | . 2 ⊢ (φ → A = B) | |
2 | eqtrd.2 | . . 3 ⊢ (φ → B = C) | |
3 | 2 | eqeq2d 2364 | . 2 ⊢ (φ → (A = B ↔ A = C)) |
4 | 1, 3 | mpbid 201 | 1 ⊢ (φ → A = C) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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-ex 1542 df-cleq 2346 |
This theorem is referenced by: eqtr2d 2386 eqtr3d 2387 eqtr4d 2388 3eqtrd 2389 3eqtrrd 2390 3eqtr2d 2391 syl5eq 2397 syl6eq 2401 rabeqbidv 2854 rabeqbidva 2855 csbidmg 3190 csbco3g 3193 difeq12d 3386 ifeq12d 3678 ifbieq2d 3682 ifbieq12d 3684 csbsng 3785 csbunig 3899 iuneq12d 3993 iinrab2 4029 riinrab 4041 cokeq12d 4237 pw1eqadj 4332 iotaint 4352 dfiota4 4372 ssfin 4470 tfinltfinlem1 4500 oddtfin 4518 opeq12d 4586 csbxpg 4813 coeq12d 4881 reseq12d 4935 imaeq12d 4943 csbrng 4966 csbresg 4976 dfxp2 5113 funprg 5149 funprgOLD 5150 imain 5172 fnco 5191 foima 5274 f1imacnv 5302 f1ococnv2 5309 fveq12d 5333 csbfv12g 5336 csbfv2g 5337 csbfvg 5338 fvun1 5379 fvresi 5443 csbov12g 5553 csbov1g 5554 csbov2g 5555 fmpt2x 5730 fvfullfun 5864 enmap2lem5 6067 enmap1lem5 6073 enprmaplem5 6080 sbthlem3 6205 muc0or 6252 nmembers1 6271 nchoicelem1 6289 nchoicelem2 6290 nchoicelem3 6291 nchoicelem7 6295 |
Copyright terms: Public domain | W3C validator |