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  4659  ftpg  7143  frrlem13  8283  brinxper  8712  sdom0  9085  funsnfsupp  9340  sucprcreg  9556  sucprcregOLD  9557  fin23lem40  10323  ffz0iswrd  14568  s4f1o  14945  fsumsplitsnun  15796  lcmcllem  16644  catcone0  17733  prmidl2  21428  lidldvgen  21462  mat1dimbas  22590  pmatcollpw3fi  22903  nbgrssvwo2  29621  wlkn0  29879  clwlkcompbp  30040  clwlkclwwlkflem  30264  konigsberglem5  30516  difininv  32773  eulerpartlemgs2  34687  bnj1476  35152  bnj1204  35317  axprALT2  35417  noinfepregs  35441  dfon2lem3  36146  bj-ccinftydisj  37717  nninfnub  38262  ispridl2  38549  rp-isfinite6  44106  fnresfnco  47633
  Copyright terms: Public domain W3C validator