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

Theorem sylbb2 239
 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 229 . 2 (𝜓𝜒)
41, 3sylbi 218 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:  ftpg  6913  wfrlem5  7953  funsnfsupp  8849  sucprcreg  9057  fin23lem40  9765  ffz0iswrd  13884  s4f1o  14273  fsumsplitsnun  15102  lcmcllem  15932  lidldvgen  19949  mat1dimbas  20997  pmatcollpw3fi  21309  nbgrssvwo2  27058  wlkn0  27316  clwlkcompbp  27477  clwlkclwwlkflem  27696  konigsberglem5  27949  difininv  30193  prmidl2  30864  eulerpartlemgs2  31524  bnj1476  32005  bnj1204  32168  dfon2lem3  32914  frrlem13  33019  bj-ccinftydisj  34374  nninfnub  34894  ispridl2  35184  rp-isfinite6  39745  fnresfnco  43138
 Copyright terms: Public domain W3C validator