| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bitr2di | Structured version Visualization version GIF version | ||
| Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
| Ref | Expression |
|---|---|
| bitr2di.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| bitr2di.2 | ⊢ (𝜒 ↔ 𝜃) |
| Ref | Expression |
|---|---|
| bitr2di | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr2di.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | bitr2di.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
| 3 | 1, 2 | bitrdi 287 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
| 4 | 3 | bicomd 223 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ 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: bitr4id 290 bibif 371 oranabs 1002 necon4bid 2986 2reu4lem 4522 resopab2 6054 xpco 6309 funconstss 7076 xpopth 8055 xpord2pred 8170 snmapen 9078 ac6sfi 9320 supgtoreq 9510 rankr1bg 9843 alephsdom 10126 brdom7disj 10571 fpwwe2lem12 10682 nn0sub 12576 elznn0 12628 nn01to3 12983 supxrbnd1 13363 supxrbnd2 13364 rexuz3 15387 smueqlem 16527 qnumdenbi 16781 dfiso3 17817 tltnle 18467 lssne0 20949 pjfval2 21729 0top 22990 1stccn 23471 dscopn 24586 bcthlem1 25358 ovolgelb 25515 iblpos 25828 itgposval 25831 itgsubstlem 26089 sincosq3sgn 26542 sincosq4sgn 26543 lgsquadlem3 27426 elzs2 28385 colinearalg 28925 elntg2 29000 wlklnwwlkln2lem 29902 2pthdlem1 29950 wwlks2onsym 29978 rusgrnumwwlkb0 29991 numclwwlk2lem1 30395 nmoo0 30810 leop3 32144 leoptri 32155 f1od2 32732 fedgmullem2 33681 dfrdg4 35952 curf 37605 poimirlem28 37655 itgaddnclem2 37686 relssinxpdmrn 38350 lfl1dim 39122 glbconxN 39380 2dim 39472 elpadd0 39811 dalawlem13 39885 diclspsn 41196 dihglb2 41344 dochsordN 41376 redvmptabs 42390 lzunuz 42779 tfsconcat0b 43359 uneqsn 44038 ntrclskb 44082 ntrneiel2 44099 infxrbnd2 45380 funressnfv 47055 funressndmafv2rn 47235 iccpartiltu 47409 |
| Copyright terms: Public domain | W3C validator |