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 277 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitri 274 | 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 353 xorneg2 1520 sbrimvw 2094 2eu4 2655 2eu5 2656 euxfrw 3677 euxfr 3679 euind 3680 rmo4 3686 rmo3f 3690 2reu5lem3 3713 rmo3 3843 difin 4219 indifdi 4241 ab0orv 4336 dftr5 5224 axsepgfromrep 5252 reusv2lem4 5354 rabxp 5676 elvvv 5703 eliunxp 5789 elidinxp 5993 imadisj 6028 idrefALT 6061 intirr 6068 resco 6198 funcnv3 6566 fncnv 6569 fun11 6570 fununi 6571 mptfnf 6631 f1mpt 7202 mpomptx 7461 uniuni 7686 frxp 8046 oeeu 8517 ixp0x 8797 xpcomco 8939 1sdomOLD 9126 dffi3 9300 wemapsolem 9419 cardval3 9821 kmlem4 10022 kmlem12 10030 kmlem14 10032 kmlem15 10033 kmlem16 10034 fpwwe2 10512 axgroth4 10701 ltexprlem4 10908 bitsmod 16250 pythagtrip 16640 isstruct 16958 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 27200 numedglnl 27893 usgr2pth0 28511 adjbd1o 30825 nmo 31216 dmrab 31222 difrab2 31223 mpomptxf 31392 ccfldextdgrr 32139 isros 32540 1stmbfm 32633 bnj976 33162 bnj1143 33175 bnj1533 33237 bnj864 33307 bnj983 33336 bnj1174 33388 bnj1175 33389 bnj1280 33405 cvmlift2lem12 33681 axacprim 34053 xpord2pred 34180 xpord2ind 34182 dfrecs2 34430 andnand1 34768 bj-snglc 35335 bj-disj2r 35394 bj-dfmpoa 35484 bj-mpomptALT 35485 mptsnunlem 35704 wl-df3xor2 35835 wl-df4-3mintru2 35853 wl-cases2-dnf 35866 wl-euae 35871 itg2addnc 36027 asindmre 36056 brres2 36623 brxrn2 36732 dfxrn2 36733 inxpxrn 36752 refsymrel2 36924 refsymrel3 36925 dfeqvrel2 36947 dfeqvrel3 36948 isopos 37537 dihglblem6 39698 dihglb2 39700 fgraphopab 41402 dflim5 41420 ifpid2g 41527 ifpim23g 41529 rp-fakeanorass 41547 en2pr 41581 elmapintrab 41610 relnonrel 41621 undmrnresiss 41638 elintima 41687 relexp0eq 41735 iunrelexp0 41736 dffrege115 42012 frege131 42028 frege133 42030 ntrneikb 42130 onfrALTlem5 42588 onfrALTlem5VD 42931 ndisj2 43023 ndmaovcom 45186 eliunxp2 46158 mpomptx2 46159 mo0sn 46649 i0oii 46701 io1ii 46702 alimp-no-surprise 46973 alsi-no-surprise 46988 |
Copyright terms: Public domain | W3C validator |