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 278 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitri 275 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 |
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 206 |
This theorem is referenced by: con2bi 354 xorneg2 1521 sbrimvw 2095 2eu4 2656 2eu5 2657 euxfrw 3678 euxfr 3680 euind 3681 rmo4 3687 rmo3f 3691 2reu5lem3 3714 rmo3 3844 difin 4220 indifdi 4242 ab0orv 4337 dftr5 5225 axsepgfromrep 5253 reusv2lem4 5355 rabxp 5677 elvvv 5704 eliunxp 5790 elidinxp 5994 imadisj 6029 idrefALT 6062 intirr 6069 resco 6199 funcnv3 6567 fncnv 6570 fun11 6571 fununi 6572 mptfnf 6632 f1mpt 7203 mpomptx 7462 uniuni 7687 frxp 8047 oeeu 8518 ixp0x 8798 xpcomco 8940 1sdomOLD 9127 dffi3 9301 wemapsolem 9420 cardval3 9822 kmlem4 10023 kmlem12 10031 kmlem14 10033 kmlem15 10034 kmlem16 10035 fpwwe2 10513 axgroth4 10702 ltexprlem4 10909 bitsmod 16251 pythagtrip 16641 isstruct 16959 pgpfac1 19788 pgpfac 19792 isassa 21185 basdif0 22225 ntreq0 22350 tgcmp 22674 tx1cn 22882 rnelfmlem 23225 phtpcer 24280 iscvsp 24413 caucfil 24569 minveclem1 24710 ovoliunlem1 24788 mdegleb 25351 eqscut2 27067 dmscut 27072 made0 27124 istrkg2ld 27188 numedglnl 27881 usgr2pth0 28499 adjbd1o 30813 nmo 31204 dmrab 31210 difrab2 31211 mpomptxf 31380 ccfldextdgrr 32127 isros 32528 1stmbfm 32621 bnj976 33150 bnj1143 33163 bnj1533 33225 bnj864 33295 bnj983 33324 bnj1174 33376 bnj1175 33377 bnj1280 33393 cvmlift2lem12 33669 axacprim 34041 xpord2pred 34168 xpord2ind 34170 dfrecs2 34421 andnand1 34759 bj-snglc 35326 bj-disj2r 35385 bj-dfmpoa 35475 bj-mpomptALT 35476 mptsnunlem 35695 wl-df3xor2 35826 wl-df4-3mintru2 35844 wl-cases2-dnf 35857 wl-euae 35862 itg2addnc 36018 asindmre 36047 brres2 36614 brxrn2 36723 dfxrn2 36724 inxpxrn 36743 refsymrel2 36915 refsymrel3 36916 dfeqvrel2 36938 dfeqvrel3 36939 isopos 37528 dihglblem6 39689 dihglb2 39691 fgraphopab 41371 dflim5 41389 ifpid2g 41496 ifpim23g 41498 rp-fakeanorass 41516 en2pr 41550 elmapintrab 41579 relnonrel 41590 undmrnresiss 41607 elintima 41656 relexp0eq 41704 iunrelexp0 41705 dffrege115 41981 frege131 41997 frege133 41999 ntrneikb 42099 onfrALTlem5 42557 onfrALTlem5VD 42900 ndisj2 42993 ndmaovcom 45137 eliunxp2 46109 mpomptx2 46110 mo0sn 46600 i0oii 46652 io1ii 46653 alimp-no-surprise 46924 alsi-no-surprise 46939 |
Copyright terms: Public domain | W3C validator |