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

Theorem sylbb2 226
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 216 . 2 (𝜓𝜒)
41, 3sylbi 205 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  ftpg  6303  wfrlem5  7280  funsnfsupp  8156  fin23lem40  9030  s4f1o  13456  fsumsplitsnun  14271  lcmcllem  15090  mat1dimbas  20036  pmatcollpw3fi  20348  usgrarnedg  25676  nbgrassvwo  25729  nbgrassvwo2  25730  nbcusgra  25755  wwlknndef  26028  clwwlknndef  26064  eulerpartlemgs2  29572  bnj1476  29974  bnj1204  30137  dfon2lem3  30737  frrlem5  30831  bj-ccinftydisj  32077  nninfnub  32517  ispridl2  32807  rp-isfinite6  36683  fnresfnco  39656  nbgrssvwo2  40586  1wlkn0  40824  konigsberglem5  41425
  Copyright terms: Public domain W3C validator