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

Theorem sylbbr 224
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 205, sylib 206, sylbir 223, sylibr 222; four inferences inferring an implication from two biconditionals: sylbb 207, sylbbr 224, sylbb1 225, sylbb2 226; four inferences inferring a biconditional from two biconditionals: bitri 262, bitr2i 263, bitr3i 264, bitr4i 265 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 45, syl5 33, syl6 34, mpbid 220, bitrd 266, syl5bb 270, syl6bb 274 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 216 . 2 (𝜒𝜓)
3 sylbbr.1 . 2 (𝜑𝜓)
42, 3sylibr 222 1 (𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  bitri  262  euelss  3872  dfnfc2  4384  ndmima  5408  axcclem  9139  fsumcom2  14293  fprodcom2  14499  pmtr3ncomlem1  17662  mdetunilem7  20185  cmpcov2  20945  f1omptsnlem  32155  igenval2  32831  mpt2bi123f  32937  brtrclfv2  36834  clsk1indlem3  37157  umgredg  40366  clwwlksnndef  41193  2pthfrgrrn  41447
  Copyright terms: Public domain W3C validator