![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylbb1 | Structured version Visualization version GIF version |
Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
Ref | Expression |
---|---|
sylbb1.1 | ⊢ (𝜑 ↔ 𝜓) |
sylbb1.2 | ⊢ (𝜑 ↔ 𝜒) |
Ref | Expression |
---|---|
sylbb1 | ⊢ (𝜓 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbb1.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | biimpri 227 | . 2 ⊢ (𝜓 → 𝜑) |
3 | sylbb1.2 | . 2 ⊢ (𝜑 ↔ 𝜒) | |
4 | 2, 3 | sylib 217 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: fsuppmapnn0fiubex 13957 rrxcph 24909 volun 25062 umgrislfupgr 28383 usgrislfuspgr 28444 wlkp1lem8 28937 elwwlks2s3 29205 eupthp1 29469 cnvbraval 31363 ballotlemfp1 33490 finixpnum 36473 fin2so 36475 matunitlindflem1 36484 oeord2com 42061 clsf2 42877 ellimcabssub0 44333 sge0iunmpt 45134 icceuelpartlem 46103 nnsum4primesodd 46464 nnsum4primesoddALTV 46465 |
Copyright terms: Public domain | W3C validator |