![]() |
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 266 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 3bitr3i.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
5 | 3, 4 | bitri 264 | 1 ⊢ (𝜒 ↔ 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 |
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 197 |
This theorem is referenced by: an12 855 xorass 1508 cbval2 2315 cbvaldva 2317 sbco2d 2444 sbcom 2446 equsb3 2460 equsb3ALT 2461 elsb3 2462 elsb4 2463 sb7f 2481 sbco4lem 2493 eq2tri 2712 eqsb3 2757 clelsb3 2758 clelsb3f 2797 r19.35 3113 ralcom4 3255 rexcom4 3256 ceqsralt 3260 gencbvex 3281 gencbval 3283 ceqsrexbv 3368 euind 3426 reuind 3444 sbccomlem 3541 sbccom 3542 csbcom 4027 difcom 4086 eqsn 4393 uniintsn 4546 disjxun 4683 reusv2lem4 4902 exss 4961 opab0 5036 elxp2OLD 5167 eqbrriv 5249 dm0rn0 5374 dfres2 5488 qfto 5552 rninxp 5608 coeq0 5682 fununi 6002 dffv2 6310 fndmin 6364 fnprb 6513 fntpb 6514 dfoprab2 6743 dfer2 7788 eceqoveq 7895 euen1 8067 xpsnen 8085 xpassen 8095 marypha2lem3 8384 rankuni 8764 card1 8832 alephislim 8944 dfacacn 9001 kmlem4 9013 ac6num 9339 zorn2lem4 9359 fpwwe2lem8 9497 fpwwe2lem12 9501 mappsrpr 9967 sqeqori 13016 trclublem 13780 fprodle 14771 vdwmc2 15730 txflf 21857 metustid 22406 caucfil 23127 ovolgelb 23294 dfcgra2 25766 axcontlem5 25893 frgr3v 27255 nmoubi 27755 hvsubaddi 28051 hlimeui 28225 omlsilem 28389 pjoml3i 28573 hodsi 28762 nmopub 28895 nmfnleub 28912 nmopcoadj0i 29090 pjin3i 29181 or3dir 29436 ralcom4f 29444 rexcom4f 29445 uniinn0 29492 ordtconnlem1 30098 bnj62 30914 bnj610 30943 bnj1143 30987 bnj1533 31048 bnj543 31089 bnj545 31091 bnj594 31108 ceqsralv2 31733 brsuccf 32173 brfullfun 32180 filnetlem4 32501 bj-ssbcom3lem 32775 bj-cbval2v 32862 bj-clelsb3 32973 icorempt2 33329 poimirlem13 33552 poimirlem14 33553 poimirlem21 33560 poimirlem22 33561 poimir 33572 sbccom2lem 34059 eldmqsres 34192 opelinxp 34251 alrmomorn 34263 xrninxp2 34291 isltrn2N 35724 moxfr 37572 ifporcor 38123 ifpancor 38125 ifpbicor 38137 ifpnorcor 38142 ifpnancor 38143 ifpororb 38167 relexp0eq 38310 hashnzfzclim 38838 pm11.6 38909 sbc3or 39055 cbvexsv 39079 sprvalpwn0 42058 copisnmnd 42134 |
Copyright terms: Public domain | W3C validator |