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 280 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 3bitr3i.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
5 | 3, 4 | bitri 278 | 1 ⊢ (𝜒 ↔ 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 |
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 210 |
This theorem is referenced by: an33rean 1485 xorass 1512 cbvaldvaw 2046 sbievw2 2103 sbco4lem 2277 sbco4lemOLD 2278 cbvexv1 2342 cbval2vOLD 2344 cbvex 2398 sbco2d 2515 sbcom 2517 sb7f 2529 eq2tri 2805 clelsb3fw 2908 clelsb3f 2909 cbvraldva2 3364 cbvrexdva2 3365 ceqsralt 3436 gencbvex 3461 gencbval 3463 ceqsrexbv 3561 euind 3634 reuind 3663 sbccomlem 3779 sbccom 3780 csbcom 4329 difcom 4397 eqsn 4739 uniintsn 4895 disjxun 5048 reusv2lem4 5291 exss 5344 opab0 5432 opelinxp 5625 eqbrriv 5658 dm0rn0 5791 elidinxp 5908 qfto 5983 rninxp 6039 coeq0 6116 fununi 6452 dffv2 6803 fndmin 6862 fnprb 7021 fntpb 7022 dfoprab2 7266 dfer2 8389 eceqoveq 8501 euen1 8700 xpsnen 8726 xpassen 8736 marypha2lem3 9050 rankuni 9476 card1 9581 alephislim 9694 dfacacn 9752 kmlem4 9764 ac6num 10090 zorn2lem4 10110 mappsrpr 10719 sqeqori 13779 trclublem 14555 fprodle 15555 vdwmc2 16529 txflf 22900 metustid 23449 caucfil 24177 ovolgelb 24374 dfcgra2 26918 axcontlem5 27056 frgr3v 28355 nmoubi 28850 hvsubaddi 29144 hlimeui 29318 omlsilem 29480 pjoml3i 29664 hodsi 29853 nmopub 29986 nmfnleub 30003 nmopcoadj0i 30181 pjin3i 30272 or3dir 30527 ralcom4f 30534 rexcom4f 30535 uniinn0 30606 ordtconnlem1 31585 bnj62 32408 bnj610 32436 bnj1143 32480 bnj1533 32542 bnj543 32583 bnj545 32585 bnj594 32602 cusgracyclt3v 32828 ceqsralv2 33382 xpab 33389 brsuccf 33977 brfullfun 33984 filnetlem4 34304 icorempo 35256 poimirlem13 35525 poimirlem14 35526 poimirlem21 35533 poimirlem22 35534 poimir 35545 sbccom2lem 36017 alrmomorn 36225 dfeldisj5 36567 isltrn2N 37869 moxfr 40215 ifporcor 40752 ifpancor 40754 ifpbicor 40765 ifpnorcor 40770 ifpnancor 40771 ifpororb 40795 relexp0eq 40984 hashnzfzclim 41611 pm11.6 41681 sbc3or 41823 cbvexsv 41838 dfich2 44581 ichbi12i 44583 sprvalpwn0 44606 copisnmnd 45034 |
Copyright terms: Public domain | W3C validator |