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

Theorem sylbbr 237
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 218, sylib 219, sylbir 236, sylibr 235; four inferences inferring an implication from two biconditionals: sylbb 220, sylbbr 237, sylbb1 238, sylbb2 239; four inferences inferring a biconditional from two biconditionals: bitri 276, bitr2i 277, bitr3i 278, bitr4i 279 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 47, syl5 34, syl6 35, mpbid 233, bitrd 280, syl5bb 284, syl6bb 288 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 229 . 2 (𝜒𝜓)
3 sylbbr.1 . 2 (𝜑𝜓)
42, 3sylibr 235 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:  bitri  276  euelss  4294  dfnfc2  4855  ndmima  5964  axcclem  9868  cshw1  14174  fsumcom2  15119  fprodcom2  15328  pmtr3ncomlem1  18521  mdetunilem7  21143  cmpcov2  21914  hausflf2  22522  umgredg  26837  vtxdginducedm1  27239  2pthfrgrrn  27975  eqdif  30195  cusgredgex2  32253  conway  33148  f1omptsnlem  34486  igenval2  35212  mpobi123f  35308  brtrclfv2  39937  clsk1indlem3  40258  or2expropbilem1  43133
  Copyright terms: Public domain W3C validator