![]() |
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 1518 sbrimvw 2089 2eu4 2653 2eu5 2654 r19.41v 3187 r3ex 3196 r19.41 3261 sbralie 3356 pm13.183 3666 euxfrw 3730 euxfr 3732 euind 3733 rmo4 3739 rmo3f 3743 2reu5lem3 3766 rmo3 3898 difin 4278 indifdi 4300 ab0orv 4389 dftr5 5269 axsepgfromrep 5300 inuni 5356 reusv2lem4 5407 rabxp 5737 elvvv 5764 eliunxp 5851 elidinxp 6064 imadisj 6100 idrefALT 6134 intirr 6141 resco 6272 funcnv3 6638 fncnv 6641 fun11 6642 fununi 6643 mptfnf 6704 f1mpt 7281 mpomptx 7546 uniuni 7781 frxp 8150 xpord2pred 8169 xpord2indlem 8171 oeeu 8640 ixp0x 8965 xpcomco 9101 1sdomOLD 9283 dffi3 9469 wemapsolem 9588 cardval3 9990 kmlem4 10192 kmlem12 10200 kmlem14 10202 kmlem15 10203 kmlem16 10204 fpwwe2 10681 axgroth4 10870 ltexprlem4 11077 bitsmod 16470 pythagtrip 16868 isstruct 17186 pgpfac1 20115 pgpfac 20119 basdif0 22976 ntreq0 23101 tgcmp 23425 tx1cn 23633 rnelfmlem 23976 phtpcer 25041 iscvsp 25175 caucfil 25331 minveclem1 25472 ovoliunlem1 25551 mdegleb 26118 eqscut2 27866 dmscut 27871 made0 27927 mulsuniflem 28190 istrkg2ld 28483 numedglnl 29176 usgr2pth0 29798 adjbd1o 32114 nmo 32518 dmrab 32525 difrab2 32526 mpomptxf 32694 ccfldextdgrr 33697 isros 34149 1stmbfm 34242 bnj976 34770 bnj1143 34783 bnj1533 34845 bnj864 34915 bnj983 34944 bnj1174 34996 bnj1175 34997 bnj1280 35013 cvmlift2lem12 35299 axacprim 35687 dfrecs2 35932 andnand1 36384 bj-snglc 36952 bj-disj2r 37011 bj-dfmpoa 37101 bj-mpomptALT 37102 mptsnunlem 37321 wl-df3xor2 37452 wl-df4-3mintru2 37470 wl-cases2-dnf 37493 wl-euae 37498 itg2addnc 37661 asindmre 37690 brres2 38250 brxrn2 38357 dfxrn2 38358 inxpxrn 38377 refsymrel2 38549 refsymrel3 38550 dfeqvrel2 38572 dfeqvrel3 38573 isopos 39162 dihglblem6 41323 dihglb2 41325 fgraphopab 43192 unielss 43207 dflim5 43319 ifpid2g 43483 ifpim23g 43485 rp-fakeanorass 43503 en2pr 43537 elmapintrab 43566 relnonrel 43577 undmrnresiss 43594 elintima 43643 relexp0eq 43691 iunrelexp0 43692 dffrege115 43968 frege131 43984 frege133 43986 ntrneikb 44084 elnev 44434 onfrALTlem5 44540 onfrALTlem5VD 44883 ndisj2 44991 ndmaovcom 47155 usgrexmpl2nb3 47929 eliunxp2 48179 mpomptx2 48180 mo0sn 48664 i0oii 48716 io1ii 48717 alimp-no-surprise 49012 alsi-no-surprise 49027 |
Copyright terms: Public domain | W3C validator |