| 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 206 |
| 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 207 |
| This theorem is referenced by: con2bi 353 xorneg2 1521 sbrimvw 2091 2eu4 2655 2eu5 2656 r19.41v 3189 r3ex 3198 r19.41 3263 sbralie 3358 pm13.183 3666 euxfrw 3727 euxfr 3729 euind 3730 rmo4 3736 rmo3f 3740 2reu5lem3 3763 rmo3 3889 difin 4272 indifdi 4294 ab0orv 4383 dftr5 5263 axsepgfromrep 5294 inuni 5350 reusv2lem4 5401 rabxp 5733 elvvv 5761 eliunxp 5848 elidinxp 6062 imadisj 6098 idrefALT 6131 intirr 6138 resco 6270 funcnv3 6636 fncnv 6639 fun11 6640 fununi 6641 mptfnf 6703 f1mpt 7281 mpomptx 7546 uniuni 7782 frxp 8151 xpord2pred 8170 xpord2indlem 8172 oeeu 8641 ixp0x 8966 xpcomco 9102 1sdomOLD 9285 dffi3 9471 wemapsolem 9590 cardval3 9992 kmlem4 10194 kmlem12 10202 kmlem14 10204 kmlem15 10205 kmlem16 10206 fpwwe2 10683 axgroth4 10872 ltexprlem4 11079 bitsmod 16473 pythagtrip 16872 isstruct 17189 pgpfac1 20100 pgpfac 20104 basdif0 22960 ntreq0 23085 tgcmp 23409 tx1cn 23617 rnelfmlem 23960 phtpcer 25027 iscvsp 25161 caucfil 25317 minveclem1 25458 ovoliunlem1 25537 mdegleb 26103 eqscut2 27851 dmscut 27856 made0 27912 mulsuniflem 28175 istrkg2ld 28468 numedglnl 29161 usgr2pth0 29785 adjbd1o 32104 nmo 32509 dmrab 32516 difrab2 32517 mpomptxf 32687 ccfldextdgrr 33722 fldextrspunlsplem 33723 isros 34169 1stmbfm 34262 bnj976 34791 bnj1143 34804 bnj1533 34866 bnj864 34936 bnj983 34965 bnj1174 35017 bnj1175 35018 bnj1280 35034 cvmlift2lem12 35319 axacprim 35707 dfrecs2 35951 andnand1 36402 bj-snglc 36970 bj-disj2r 37029 bj-dfmpoa 37119 bj-mpomptALT 37120 mptsnunlem 37339 wl-df3xor2 37470 wl-df4-3mintru2 37488 wl-cases2-dnf 37513 wl-euae 37518 itg2addnc 37681 asindmre 37710 brres2 38269 brxrn2 38376 dfxrn2 38377 inxpxrn 38396 refsymrel2 38568 refsymrel3 38569 dfeqvrel2 38591 dfeqvrel3 38592 isopos 39181 dihglblem6 41342 dihglb2 41344 fgraphopab 43215 unielss 43230 dflim5 43342 ifpid2g 43506 ifpim23g 43508 rp-fakeanorass 43526 en2pr 43560 elmapintrab 43589 relnonrel 43600 undmrnresiss 43617 elintima 43666 relexp0eq 43714 iunrelexp0 43715 dffrege115 43991 frege131 44007 frege133 44009 ntrneikb 44107 elnev 44457 onfrALTlem5 44562 onfrALTlem5VD 44905 ndisj2 45056 ndmaovcom 47217 usgrexmpl2nb3 47993 eliunxp2 48250 mpomptx2 48251 mo0sn 48735 i0oii 48817 io1ii 48818 alimp-no-surprise 49300 alsi-no-surprise 49315 |
| Copyright terms: Public domain | W3C validator |