![]() |
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 2399 sbco2d 2512 sbcom 2514 sb7f 2525 eq2tri 2800 clelsb2OLD 2863 clelsb1fw 2908 clelsb1f 2909 cbvraldva 3237 rexcom 3288 cbvrexfw 3303 cbvraldva2 3345 cbvrexdva2OLD 3347 sbralie 3355 ceqsralt 3506 gencbvex 3534 gencbval 3536 ceqsrexbv 3642 ceqsralbv 3643 euind 3718 reuind 3747 sbccomlem 3862 sbccom 3863 csbcom 4415 difcom 4484 eqsn 4828 uniintsn 4987 disjxun 5142 reusv2lem4 5395 exss 5459 opab0 5550 opelinxp 5750 eqbrriv 5786 dm0rn0 5919 elidinxp 6036 qfto 6114 rninxp 6170 coeq0 6246 fununi 6615 dffv2 6975 fndmin 7034 fnprb 7197 fntpb 7198 dfoprab2 7454 frpoins3xp3g 8114 dfer2 8692 eceqoveq 8804 euen1 9014 xpsnen 9043 xpassen 9054 marypha2lem3 9419 rankuni 9845 card1 9950 alephislim 10065 dfacacn 10123 kmlem4 10135 ac6num 10461 zorn2lem4 10481 mappsrpr 11090 sqeqori 14165 trclublem 14929 fprodle 15927 vdwmc2 16899 txflf 23479 metustid 24032 caucfil 24769 ovolgelb 24966 dfcgra2 28048 axcontlem5 28193 frgr3v 29495 nmoubi 29990 hvsubaddi 30284 hlimeui 30458 omlsilem 30620 pjoml3i 30804 hodsi 30993 nmopub 31126 nmfnleub 31143 nmopcoadj0i 31321 pjin3i 31412 or3dir 31667 ralcom4f 31674 rexcom4f 31675 uniinn0 31748 ordtconnlem1 32835 bnj62 33662 bnj610 33689 bnj1143 33732 bnj1533 33794 bnj543 33835 bnj545 33837 bnj594 33854 cusgracyclt3v 34078 xpab 34626 brsuccf 34844 brfullfun 34851 filnetlem4 35171 icorempo 36137 poimirlem13 36406 poimirlem14 36407 poimirlem21 36414 poimirlem22 36415 poimir 36426 sbccom2lem 36898 alrmomorn 37133 dfeldisj5 37497 mpet2 37616 isltrn2N 38897 moxfr 41301 ifporcor 42084 ifpancor 42086 ifpbicor 42097 ifpnorcor 42102 ifpnancor 42103 ifpororb 42127 minregex 42156 relexp0eq 42323 hashnzfzclim 42952 pm11.6 43022 sbc3or 43164 cbvexsv 43179 dfich2 45999 ichbi12i 46001 sprvalpwn0 46024 copisnmnd 46452 |
Copyright terms: Public domain | W3C validator |