| 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 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: an33rean 1485 xorass 1515 cbvaldvaw 2037 sbievw2 2098 sbco4lemOLD 2174 cbvexv1 2344 cbvex 2404 sbco2d 2517 sbcom 2519 sb7f 2530 eq2tri 2804 clelsb2OLD 2870 clelsb1fw 2909 clelsb1f 2910 cbvraldva 3239 rexcom 3290 cbvrexfw 3305 cbvraldva2 3348 cbvrexdva2OLD 3350 sbralie 3358 ceqsralt 3516 gencbvex 3541 gencbval 3543 ceqsrexbv 3656 ceqsralbv 3657 euind 3730 reuind 3759 sbccomlem 3869 sbccomlemOLD 3870 sbccom 3871 csbcom 4420 difcom 4489 eqsn 4829 uniintsn 4985 disjxun 5141 reusv2lem4 5401 exss 5468 opab0 5559 opelinxp 5765 eqbrriv 5801 dm0rn0 5935 elidinxp 6062 qfto 6141 rninxp 6199 coeq0 6275 fununi 6641 dffv2 7004 fndmin 7065 fnprb 7228 fntpb 7229 dfoprab2 7491 frpoins3xp3g 8166 dfer2 8746 eceqoveq 8862 euen1 9067 xpsnen 9095 xpassen 9106 marypha2lem3 9477 rankuni 9903 card1 10008 alephislim 10123 dfacacn 10182 kmlem4 10194 ac6num 10519 zorn2lem4 10539 mappsrpr 11148 sqeqori 14253 trclublem 15034 fprodle 16032 vdwmc2 17017 txflf 24014 metustid 24567 caucfil 25317 ovolgelb 25515 dfcgra2 28838 axcontlem5 28983 frgr3v 30294 nmoubi 30791 hvsubaddi 31085 hlimeui 31259 omlsilem 31421 pjoml3i 31605 hodsi 31794 nmopub 31927 nmfnleub 31944 nmopcoadj0i 32122 pjin3i 32213 an42ds 32469 or3dir 32479 ralcom4f 32486 rexcom4f 32487 uniinn0 32563 ordtconnlem1 33923 bnj62 34734 bnj610 34761 bnj1143 34804 bnj1533 34866 bnj543 34907 bnj545 34909 bnj594 34926 cusgracyclt3v 35161 xpab 35726 brsuccf 35942 brfullfun 35949 in-ax8 36225 filnetlem4 36382 icorempo 37352 poimirlem13 37640 poimirlem14 37641 poimirlem21 37648 poimirlem22 37649 poimir 37660 sbccom2lem 38131 alrmomorn 38359 dfeldisj5 38722 mpet2 38841 isltrn2N 40122 moxfr 42703 ifporcor 43475 ifpancor 43477 ifpbicor 43488 ifpnorcor 43493 ifpnancor 43494 ifpororb 43518 minregex 43547 relexp0eq 43714 hashnzfzclim 44341 pm11.6 44411 sbc3or 44552 cbvexsv 44567 dfich2 47445 ichbi12i 47447 sprvalpwn0 47470 copisnmnd 48085 |
| Copyright terms: Public domain | W3C validator |