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

Theorem sylbb2 237
Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)
Hypotheses
Ref Expression
sylbb2.1 (𝜑𝜓)
sylbb2.2 (𝜒𝜓)
Assertion
Ref Expression
sylbb2 (𝜑𝜒)

Proof of Theorem sylbb2
StepHypRef Expression
1 sylbb2.1 . 2 (𝜑𝜓)
2 sylbb2.2 . . 3 (𝜒𝜓)
32biimpri 227 . 2 (𝜓𝜒)
41, 3sylbi 216 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  rexprg  4701  ftpg  7154  frrlem13  8283  wfrlem5OLD  8313  sdom0  9108  funsnfsupp  9387  sucprcreg  9596  fin23lem40  10346  ffz0iswrd  14491  s4f1o  14869  fsumsplitsnun  15701  lcmcllem  16533  catcone0  17631  lidldvgen  20893  mat1dimbas  21974  pmatcollpw3fi  22287  nbgrssvwo2  28650  wlkn0  28909  clwlkcompbp  29070  clwlkclwwlkflem  29288  konigsberglem5  29540  difininv  31786  prmidl2  32590  eulerpartlemgs2  33410  bnj1476  33889  bnj1204  34054  dfon2lem3  34788  bj-ccinftydisj  36142  nninfnub  36667  ispridl2  36954  rp-isfinite6  42317  fnresfnco  45799
  Copyright terms: Public domain W3C validator