New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > bitr2i | GIF version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr2i.1 | ⊢ (φ ↔ ψ) |
bitr2i.2 | ⊢ (ψ ↔ χ) |
Ref | Expression |
---|---|
bitr2i | ⊢ (χ ↔ φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2i.1 | . . 3 ⊢ (φ ↔ ψ) | |
2 | bitr2i.2 | . . 3 ⊢ (ψ ↔ χ) | |
3 | 1, 2 | bitri 240 | . 2 ⊢ (φ ↔ χ) |
4 | 3 | bicomi 193 | 1 ⊢ (χ ↔ φ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: 3bitrri 263 3bitr2ri 265 3bitr4ri 269 nan 563 pm4.15 564 pm5.17 858 pm4.83 895 pm5.7 900 3or6 1263 nanim 1292 hadnot 1393 19.12vv 1898 2exsb 2132 2eu4 2287 cvjust 2348 abbi 2463 spc3gv 2944 sbc8g 3053 ss2rab 3342 difdif 3392 ddif 3398 unass 3420 unss 3437 undi 3502 rabeq0 3572 disj 3591 ssindif0 3604 pwsnALT 3882 dfpss4 3888 iinrab2 4029 imacok 4282 dfaddc2 4381 dfnnc2 4395 nnsucelr 4428 tfinnn 4534 eqvinop 4606 unopab 4638 elswap 4740 dfswap2 4741 ssrnres 5059 cnvresima 5077 coundi 5082 coundir 5083 coass 5097 fun11 5159 fununi 5160 funcnvuni 5161 fsn 5432 fconstfv 5456 eloprabga 5578 funoprabg 5583 releqmpt2 5809 funsex 5828 brpprod 5839 fvfullfunlem1 5861 enpw1lem1 6061 enpw1pw 6075 lecex 6115 nncdiv3lem1 6275 nchoicelem11 6299 |
Copyright terms: Public domain | W3C validator |