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 229 | . 2 ⊢ (𝜓 → 𝜑) |
3 | sylbb1.2 | . 2 ⊢ (𝜑 ↔ 𝜒) | |
4 | 2, 3 | sylib 219 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: fsuppmapnn0fiubex 13348 rrxcph 23922 volun 24073 umgrislfupgr 26835 usgrislfuspgr 26896 wlkp1lem8 27389 elwwlks2s3 27657 eupthp1 27922 cnvbraval 29814 ballotlemfp1 31648 finixpnum 34758 fin2so 34760 matunitlindflem1 34769 clsf2 40354 ellimcabssub0 41774 sge0iunmpt 42577 icceuelpartlem 43472 nnsum4primesodd 43838 nnsum4primesoddALTV 43839 |
Copyright terms: Public domain | W3C validator |