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

Theorem sylbb2 228
 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 218 . 2 (𝜓𝜒)
41, 3sylbi 207 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  ftpg  6388  wfrlem5  7379  funsnfsupp  8259  fin23lem40  9133  s4f1o  13615  fsumsplitsnun  14433  lcmcllem  15252  mat1dimbas  20218  pmatcollpw3fi  20530  nbgrssvwo2  26182  wlkn0  26420  konigsberglem5  27018  eulerpartlemgs2  30265  bnj1476  30678  bnj1204  30841  dfon2lem3  31444  frrlem5  31538  bj-ccinftydisj  32772  nninfnub  33218  ispridl2  33508  rp-isfinite6  37384  fnresfnco  40540
 Copyright terms: Public domain W3C validator