![]() |
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 353 xorneg2 1514 sbrimvw 2086 2eu4 2642 2eu5 2643 sbralie 3346 euxfrw 3709 euxfr 3711 euind 3712 rmo4 3718 rmo3f 3722 2reu5lem3 3745 rmo3 3875 difin 4253 indifdi 4275 ab0orv 4370 dftr5 5259 axsepgfromrep 5287 reusv2lem4 5389 rabxp 5714 elvvv 5741 eliunxp 5827 elidinxp 6033 imadisj 6069 idrefALT 6102 intirr 6109 resco 6239 funcnv3 6608 fncnv 6611 fun11 6612 fununi 6613 mptfnf 6675 f1mpt 7252 mpomptx 7513 uniuni 7742 frxp 8106 xpord2pred 8125 xpord2indlem 8127 oeeu 8598 ixp0x 8915 xpcomco 9057 1sdomOLD 9244 dffi3 9421 wemapsolem 9540 cardval3 9942 kmlem4 10143 kmlem12 10151 kmlem14 10153 kmlem15 10154 kmlem16 10155 fpwwe2 10633 axgroth4 10822 ltexprlem4 11029 bitsmod 16373 pythagtrip 16763 isstruct 17081 pgpfac1 19987 pgpfac 19991 basdif0 22766 ntreq0 22891 tgcmp 23215 tx1cn 23423 rnelfmlem 23766 phtpcer 24831 iscvsp 24965 caucfil 25121 minveclem1 25262 ovoliunlem1 25341 mdegleb 25910 eqscut2 27643 dmscut 27648 made0 27704 mulsuniflem 27953 istrkg2ld 28135 numedglnl 28828 usgr2pth0 29446 adjbd1o 31762 nmo 32154 dmrab 32161 difrab2 32162 mpomptxf 32329 ccfldextdgrr 33192 isros 33621 1stmbfm 33714 bnj976 34243 bnj1143 34256 bnj1533 34318 bnj864 34388 bnj983 34417 bnj1174 34469 bnj1175 34470 bnj1280 34486 cvmlift2lem12 34760 axacprim 35137 dfrecs2 35383 andnand1 35742 bj-snglc 36306 bj-disj2r 36365 bj-dfmpoa 36455 bj-mpomptALT 36456 mptsnunlem 36675 wl-df3xor2 36806 wl-df4-3mintru2 36824 wl-cases2-dnf 36837 wl-euae 36842 itg2addnc 36998 asindmre 37027 brres2 37592 brxrn2 37701 dfxrn2 37702 inxpxrn 37721 refsymrel2 37893 refsymrel3 37894 dfeqvrel2 37916 dfeqvrel3 37917 isopos 38506 dihglblem6 40667 dihglb2 40669 fgraphopab 42407 unielss 42422 dflim5 42534 ifpid2g 42699 ifpim23g 42701 rp-fakeanorass 42719 en2pr 42753 elmapintrab 42782 relnonrel 42793 undmrnresiss 42810 elintima 42859 relexp0eq 42907 iunrelexp0 42908 dffrege115 43184 frege131 43200 frege133 43202 ntrneikb 43300 elnev 43652 onfrALTlem5 43758 onfrALTlem5VD 44101 ndisj2 44192 ndmaovcom 46364 eliunxp2 47164 mpomptx2 47165 mo0sn 47654 i0oii 47706 io1ii 47707 alimp-no-surprise 47982 alsi-no-surprise 47997 |
Copyright terms: Public domain | W3C validator |