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

Theorem sylbb2 241
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 231 . 2 (𝜓𝜒)
41, 3sylbi 220 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  rexprg  4588  ftpg  6931  wfrlem5  7991  funsnfsupp  8933  sucprcreg  9141  fin23lem40  9854  ffz0iswrd  13985  s4f1o  14372  fsumsplitsnun  15206  lcmcllem  16040  catcone0  17064  lidldvgen  20150  mat1dimbas  21226  pmatcollpw3fi  21539  nbgrssvwo2  27307  wlkn0  27565  clwlkcompbp  27726  clwlkclwwlkflem  27944  konigsberglem5  28196  difininv  30441  prmidl2  31191  eulerpartlemgs2  31920  bnj1476  32401  bnj1204  32566  dfon2lem3  33338  frrlem13  33458  bj-ccinftydisj  35028  nninfnub  35555  ispridl2  35842  rp-isfinite6  40702  fnresfnco  44097
  Copyright terms: Public domain W3C validator