![]() |
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 270 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3bitr2i.3 | . 2 ⊢ (𝜒 ↔ 𝜃) | |
5 | 3, 4 | bitri 267 | 1 ⊢ (𝜑 ↔ 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 |
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 199 |
This theorem is referenced by: con2bi 345 an13 637 xorneg2 1592 2eu4 2685 2eu5 2686 euxfr 3604 euind 3605 rmo4 3611 rmo3f 3615 2reu5lem3 3632 rmo3 3745 rmo3OLD 3746 difin 4088 reusv2lem4 5113 rabxp 5400 elvvv 5424 eliunxp 5505 elidinxp 5705 imadisj 5738 idrefALT 5763 intirr 5769 resco 5893 funcnv3 6204 fncnv 6207 fun11 6208 fununi 6209 mptfnf 6261 f1mpt 6790 mpt2mptx 7028 uniuni 7248 frxp 7568 oeeu 7967 ixp0x 8222 xpcomco 8338 1sdom 8451 dffi3 8625 wemapsolem 8744 cardval3 9111 kmlem4 9310 kmlem12 9318 kmlem14 9320 kmlem15 9321 kmlem16 9322 fpwwe2 9800 axgroth4 9989 ltexprlem4 10196 bitsmod 15564 pythagtrip 15943 isstruct 16268 pgpfac1 18866 pgpfac 18870 isassa 19712 basdif0 21165 ntreq0 21289 tgcmp 21613 tx1cn 21821 rnelfmlem 22164 phtpcer 23202 iscvsp 23335 caucfil 23489 minveclem1 23630 ovoliunlem1 23706 mdegleb 24261 istrkg2ld 25811 numedglnl 26493 usgr2pth0 27117 adjbd1o 29516 nmo 29897 difrab2 29901 mpt2mptxf 30043 isros 30829 1stmbfm 30920 bnj976 31447 bnj1143 31460 bnj1533 31521 bnj864 31591 bnj983 31620 bnj1174 31670 bnj1175 31671 bnj1280 31687 cvmlift2lem12 31895 axacprim 32181 dmscut 32507 dfrecs2 32646 andnand1 32984 bj-dfssb2 33230 bj-denotes 33427 bj-snglc 33529 bj-disj2r 33585 bj-dfmpt2a 33644 bj-mpt2mptALT 33645 mptsnunlem 33781 wl-cases2-dnf 33890 wl-euae 33895 wl-dfralv 33980 itg2addnc 34091 asindmre 34122 brres2 34669 brxrn2 34767 dfxrn2 34768 inxpxrn 34783 refsymrel2 34943 refsymrel3 34944 dfeqvrel2 34964 dfeqvrel3 34965 isopos 35336 dihglblem6 37496 dihglb2 37498 fgraphopab 38751 ifpid2g 38800 ifpim23g 38802 rp-fakeanorass 38820 elmapintrab 38843 relintabex 38848 relnonrel 38854 undmrnresiss 38871 elintima 38906 relexp0eq 38954 iunrelexp0 38955 dffrege115 39232 frege131 39248 frege133 39250 ntrneikb 39352 onfrALTlem5 39706 onfrALTlem5VD 40058 ndisj2 40154 ndmaovcom 42250 eliunxp2 43131 mpt2mptx2 43132 alimp-no-surprise 43637 alsi-no-surprise 43652 |
Copyright terms: Public domain | W3C validator |