|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > bitr3di | Structured version Visualization version GIF version | ||
| Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) | 
| Ref | Expression | 
|---|---|
| bitr3di.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | 
| bitr3di.2 | ⊢ (𝜓 ↔ 𝜃) | 
| Ref | Expression | 
|---|---|
| bitr3di | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | bitr3di.2 | . . 3 ⊢ (𝜓 ↔ 𝜃) | |
| 2 | 1 | bicomi 224 | . 2 ⊢ (𝜃 ↔ 𝜓) | 
| 3 | bitr3di.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 4 | 2, 3 | bitr2id 284 | 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: sbco3 2517 necon2bbid 2983 notzfaus 5362 fressnfv 7179 eluniima 7271 dfac2b 10172 alephval2 10613 adderpqlem 10995 1idpr 11070 leloe 11348 negeq0 11564 addeq0 11687 muleqadd 11908 addltmul 12504 xrleloe 13187 fzrev 13628 mod0 13917 modirr 13984 cjne0 15203 lenegsq 15360 fsumsplit 15778 sumsplit 15805 dvdsabseq 16351 xpsfrnel 17608 isacs2 17697 acsfn 17703 comfeq 17750 sgrp2nmndlem3 18939 resscntz 19352 gexdvds 19603 hauscmplem 23415 hausdiag 23654 utop3cls 24261 affineequivne 26871 eqscut2 27852 ltgov 28606 ax5seglem4 28948 mdsl2i 32342 rspc2daf 32486 cycpmco2 33154 pl1cn 33955 fineqvpow 35111 satefvfmla1 35431 bj-isrvec 37296 topdifinfeq 37352 finxpreclem6 37398 wl-sb8ft 37552 ftc1anclem5 37705 fdc1 37754 relcnveq 38324 relcnveq2 38325 elrelscnveq 38494 elrelscnveq2 38495 lcvexchlem1 39036 lkreqN 39172 glbconxN 39381 islpln5 39538 islvol5 39582 cdlemefrs29bpre0 40399 cdlemg17h 40671 cdlemg33b 40710 tfsconcat0i 43363 tfsconcat0b 43364 oadif1lem 43397 oadif1 43398 brnonrel 43607 frege92 43973 e2ebind 44588 stoweidlem28 46048 clnbupgrel 47826 0funcg2 48933 | 
| Copyright terms: Public domain | W3C validator |