Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbbr Structured version   Visualization version   GIF version

Theorem sylbbr 225
 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.)
Hypotheses
Ref Expression
sylbbr.1 (𝜑𝜓)
sylbbr.2 (𝜓𝜒)
Assertion
Ref Expression
sylbbr (𝜒𝜑)

Proof of Theorem sylbbr
StepHypRef Expression
1 sylbbr.2 . . 3 (𝜓𝜒)
21biimpri 217 . 2 (𝜒𝜓)
3 sylbbr.1 . 2 (𝜑𝜓)
42, 3sylibr 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