Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitr2i | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr2i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr2i.2 | ⊢ (𝜒 ↔ 𝜓) |
3bitr2i.3 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
3bitr2i | ⊢ (𝜑 ↔ 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 3bitr2i.2 | . . 3 ⊢ (𝜒 ↔ 𝜓) | |
3 | 1, 2 | bitr4i 279 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitri 276 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 |
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 208 |
This theorem is referenced by: con2bi 355 xorneg2 1505 sbrimvlem 2092 dfsb7OLD 2278 2eu4 2737 2eu5 2738 2eu5OLD 2739 euxfrw 3711 euxfr 3713 euind 3714 rmo4 3720 rmo3f 3724 2reu5lem3 3747 rmo3 3871 rmo3OLD 3872 difin 4237 axsepgfromrep 5193 reusv2lem4 5293 rabxp 5594 elvvv 5621 eliunxp 5702 elidinxp 5905 imadisj 5942 idrefALT 5967 intirr 5972 resco 6097 funcnv3 6418 fncnv 6421 fun11 6422 fununi 6423 mptfnf 6477 f1mpt 7010 mpomptx 7254 uniuni 7472 frxp 7811 oeeu 8219 ixp0x 8479 xpcomco 8596 1sdom 8710 dffi3 8884 wemapsolem 9003 cardval3 9370 kmlem4 9568 kmlem12 9576 kmlem14 9578 kmlem15 9579 kmlem16 9580 fpwwe2 10054 axgroth4 10243 ltexprlem4 10450 bitsmod 15775 pythagtrip 16161 isstruct 16486 pgpfac1 19133 pgpfac 19137 isassa 20018 basdif0 21491 ntreq0 21615 tgcmp 21939 tx1cn 22147 rnelfmlem 22490 phtpcer 23528 iscvsp 23661 caucfil 23815 minveclem1 23956 ovoliunlem1 24032 mdegleb 24587 istrkg2ld 26174 numedglnl 26857 usgr2pth0 27474 adjbd1o 29790 nelbOLD 30160 nmo 30182 dmrab 30188 difrab2 30189 mpomptxf 30354 ccfldextdgrr 30957 isros 31327 1stmbfm 31418 bnj976 31949 bnj1143 31962 bnj1533 32024 bnj864 32094 bnj983 32123 bnj1174 32173 bnj1175 32174 bnj1280 32190 cvmlift2lem12 32459 axacprim 32831 dmscut 33170 dfrecs2 33309 andnand1 33647 bj-denotes 34086 bj-snglc 34179 bj-disj2r 34238 bj-dfmpoa 34303 bj-mpomptALT 34304 mptsnunlem 34502 wl-cases2-dnf 34635 wl-euae 34640 wl-dfralv 34723 itg2addnc 34828 asindmre 34859 brres2 35412 brxrn2 35509 dfxrn2 35510 inxpxrn 35525 refsymrel2 35685 refsymrel3 35686 dfeqvrel2 35707 dfeqvrel3 35708 isopos 36198 dihglblem6 38358 dihglb2 38360 fgraphopab 39690 ifpid2g 39739 ifpim23g 39741 rp-fakeanorass 39759 en2pr 39786 elmapintrab 39816 relnonrel 39827 undmrnresiss 39844 elintima 39878 relexp0eq 39926 iunrelexp0 39927 dffrege115 40204 frege131 40220 frege133 40222 ntrneikb 40324 onfrALTlem5 40756 onfrALTlem5VD 41099 ndisj2 41193 ndmaovcom 43285 eliunxp2 44280 mpomptx2 44281 alimp-no-surprise 44780 alsi-no-surprise 44795 |
Copyright terms: Public domain | W3C validator |