Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sylbbr | Structured version Visualization version GIF version |
Description: A mixed syllogism
inference from two biconditionals.
Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 17 infers an implication from two implications (and there are 3syl 18 and 4syl 19 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 206, sylib 207, sylbir 224, sylibr 223; four inferences inferring an implication from two biconditionals: sylbb 208, sylbbr 225, sylbb1 226, sylbb2 227; four inferences inferring a biconditional from two biconditionals: bitri 263, bitr2i 264, bitr3i 265, bitr4i 266 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 46, syl5 33, syl6 34, mpbid 221, bitrd 267, syl5bb 271, syl6bb 275 and variants. (Contributed by BJ, 21-Apr-2019.) |
Ref | Expression |
---|---|
sylbbr.1 | ⊢ (𝜑 ↔ 𝜓) |
sylbbr.2 | ⊢ (𝜓 ↔ 𝜒) |
Ref | Expression |
---|---|
sylbbr | ⊢ (𝜒 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbbr.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
2 | 1 | biimpri 217 | . 2 ⊢ (𝜒 → 𝜓) |
3 | sylbbr.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
4 | 2, 3 | sylibr 223 | 1 ⊢ (𝜒 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: bitri 263 euelss 3873 dfnfc2 4390 ndmima 5421 axcclem 9162 fsumcom2 14347 fprodcom2 14553 pmtr3ncomlem1 17716 mdetunilem7 20243 cmpcov2 21003 umgredg 25812 f1omptsnlem 32359 igenval2 33035 mpt2bi123f 33141 brtrclfv2 37038 clsk1indlem3 37361 clwwlksnndef 41198 2pthfrgrrn 41452 |
Copyright terms: Public domain | W3C validator |