![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr3i | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
Ref | Expression |
---|---|
3bitr3i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr3i.2 | ⊢ (𝜑 ↔ 𝜒) |
3bitr3i.3 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
3bitr3i | ⊢ (𝜒 ↔ 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3i.2 | . . 3 ⊢ (𝜑 ↔ 𝜒) | |
2 | 3bitr3i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | bitr3i 277 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 3bitr3i.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: an33rean 1484 xorass 1515 cbvaldvaw 2042 sbievw2 2100 sbco4lem 2273 sbco4lemOLD 2274 cbvexv1 2339 cbvex 2398 sbco2d 2515 sbcom 2517 sb7f 2529 eq2tri 2804 clelsb2OLD 2867 clelsb1fw 2912 clelsb1f 2913 rexcom 3274 cbvrexfw 3289 cbvraldva2 3324 cbvrexdva2OLD 3326 ceqsralt 3477 gencbvex 3505 gencbval 3507 ceqsrexbv 3607 ceqsralbv 3608 euind 3683 reuind 3712 sbccomlem 3827 sbccom 3828 csbcom 4378 difcom 4447 eqsn 4790 uniintsn 4949 disjxun 5104 reusv2lem4 5357 exss 5421 opab0 5512 opelinxp 5712 eqbrriv 5748 dm0rn0 5881 elidinxp 5998 qfto 6076 rninxp 6132 coeq0 6208 fununi 6577 dffv2 6937 fndmin 6996 fnprb 7159 fntpb 7160 dfoprab2 7416 frpoins3xp3g 8074 dfer2 8650 eceqoveq 8762 euen1 8971 xpsnen 9000 xpassen 9011 marypha2lem3 9374 rankuni 9800 card1 9905 alephislim 10020 dfacacn 10078 kmlem4 10090 ac6num 10416 zorn2lem4 10436 mappsrpr 11045 sqeqori 14119 trclublem 14881 fprodle 15880 vdwmc2 16852 txflf 23360 metustid 23913 caucfil 24650 ovolgelb 24847 dfcgra2 27775 axcontlem5 27920 frgr3v 29222 nmoubi 29717 hvsubaddi 30011 hlimeui 30185 omlsilem 30347 pjoml3i 30531 hodsi 30720 nmopub 30853 nmfnleub 30870 nmopcoadj0i 31048 pjin3i 31139 or3dir 31394 ralcom4f 31401 rexcom4f 31402 uniinn0 31472 ordtconnlem1 32508 bnj62 33335 bnj610 33362 bnj1143 33405 bnj1533 33467 bnj543 33508 bnj545 33510 bnj594 33527 cusgracyclt3v 33753 xpab 34300 brsuccf 34529 brfullfun 34536 filnetlem4 34856 icorempo 35825 poimirlem13 36094 poimirlem14 36095 poimirlem21 36102 poimirlem22 36103 poimir 36114 sbccom2lem 36586 alrmomorn 36822 dfeldisj5 37186 mpet2 37305 isltrn2N 38586 moxfr 41018 ifporcor 41741 ifpancor 41743 ifpbicor 41754 ifpnorcor 41759 ifpnancor 41760 ifpororb 41784 minregex 41813 relexp0eq 41980 hashnzfzclim 42609 pm11.6 42679 sbc3or 42821 cbvexsv 42836 dfich2 45657 ichbi12i 45659 sprvalpwn0 45682 copisnmnd 46110 |
Copyright terms: Public domain | W3C validator |