![]() |
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 227 | . 2 ⊢ (𝜃 ↔ 𝜓) |
3 | bitr3di.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | syl5rbb 287 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ 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: sbco3 2533 necon2bbid 2992 notzfaus 5223 fressnfv 6906 eluniima 6994 dfac2b 9575 alephval2 10017 adderpqlem 10399 1idpr 10474 leloe 10750 negeq0 10963 addeq0 11086 muleqadd 11307 addltmul 11895 xrleloe 12563 fzrev 13004 mod0 13278 modirr 13344 cjne0 14555 lenegsq 14713 fsumsplit 15130 sumsplit 15156 dvdsabseq 15699 xpsfrnel 16878 isacs2 16967 acsfn 16973 comfeq 17019 sgrp2nmndlem3 18141 resscntz 18514 gexdvds 18761 hauscmplem 22091 hausdiag 22330 utop3cls 22937 affineequivne 25497 ltgov 26475 ax5seglem4 26810 mdsl2i 30189 rspc2daf 30322 cycpmco2 30911 pl1cn 31411 satefvfmla1 32888 eqscut2 33546 topdifinfeq 35032 finxpreclem6 35078 ftc1anclem5 35399 fdc1 35449 relcnveq 36004 relcnveq2 36005 elrelscnveq 36157 elrelscnveq2 36158 lcvexchlem1 36595 lkreqN 36731 glbconxN 36939 islpln5 37096 islvol5 37140 cdlemefrs29bpre0 37957 cdlemg17h 38229 cdlemg33b 38268 brnonrel 40647 frege92 41014 e2ebind 41627 stoweidlem28 43021 |
Copyright terms: Public domain | W3C validator |