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

Theorem sylbbr 236
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 217, sylib 218, sylbir 235, sylibr 234; four inferences inferring an implication from two biconditionals: sylbb 219, sylbbr 236, sylbb1 237, sylbb2 238; four inferences inferring a biconditional from two biconditionals: bitri 275, bitr2i 276, bitr3i 277, bitr4i 278 (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 232, bitrd 279, bitrid 283, bitrdi 287 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 228 . 2 (𝜒𝜓)
3 sylbbr.1 . 2 (𝜑𝜓)
42, 3sylibr 234 1 (𝜒𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  bitri  275  euelss  4338  dfnfc2  4934  ndmima  6124  unfi  9210  axcclem  10495  cshw1  14857  fsumcom2  15807  fprodcom2  16017  pmtr3ncomlem1  19506  mdetunilem7  22640  cmpcov2  23414  hausflf2  24022  conway  27859  umgredg  29170  vtxdginducedm1  29576  2pthfrgrrn  30311  eqdif  32547  cusgredgex2  35107  f1omptsnlem  37319  igenval2  38053  mpobi123f  38149  brtrclfv2  43717  clsk1indlem3  44033  or2expropbilem1  46982  grtriproplem  47844  mo0sn  48664
  Copyright terms: Public domain W3C validator