| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3bitr2rd | Structured version Visualization version GIF version | ||
| Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
| Ref | Expression |
|---|---|
| 3bitr2d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| 3bitr2d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
| 3bitr2d.3 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
| Ref | Expression |
|---|---|
| 3bitr2rd | ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3bitr2d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 3bitr2d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) | |
| 3 | 1, 2 | bitr4d 282 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
| 4 | 3bitr2d.3 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
| 5 | 3, 4 | bitr2d 280 | 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: fnsuppres 8216 addsubeq4 11523 muleqadd 11907 mulle0b 12139 adddivflid 13858 om2uzlti 13991 summodnegmod 16324 qnumdenbi 16781 dprdf11 20043 lvecvscan2 21114 mdetunilem9 22626 elfilss 23884 mbfmulc2lem 25682 itg2seq 25777 itg2cnlem2 25797 chpchtsum 27263 bposlem7 27334 lgsdilem 27368 lgsne0 27379 colhp 28778 axcontlem7 28985 pjnorm2 31746 cdj3lem1 32453 zringfrac 33582 ply1dg1rt 33604 zrhchr 33975 bj-gabima 36941 dochfln0 41479 mapdindp 41673 stgredgiun 47925 |
| Copyright terms: Public domain | W3C validator |