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

Theorem sylbb2 238
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 228 . 2 (𝜓𝜒)
41, 3sylbi 217 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  rexprg  4697  ftpg  7176  frrlem13  8323  wfrlem5OLD  8353  brinxper  8774  sdom0  9148  funsnfsupp  9432  sucprcreg  9641  fin23lem40  10391  ffz0iswrd  14579  s4f1o  14957  fsumsplitsnun  15791  lcmcllem  16633  catcone0  17730  lidldvgen  21344  mat1dimbas  22478  pmatcollpw3fi  22791  nbgrssvwo2  29379  wlkn0  29639  clwlkcompbp  29802  clwlkclwwlkflem  30023  konigsberglem5  30275  difininv  32536  prmidl2  33469  eulerpartlemgs2  34382  bnj1476  34861  bnj1204  35026  dfon2lem3  35786  bj-ccinftydisj  37214  nninfnub  37758  ispridl2  38045  rp-isfinite6  43531  fnresfnco  47053
  Copyright terms: Public domain W3C validator