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

Theorem sylanblrc 591
Description: Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)
Hypotheses
Ref Expression
sylanblrc.1 (𝜑𝜓)
sylanblrc.2 𝜒
sylanblrc.3 (𝜃 ↔ (𝜓𝜒))
Assertion
Ref Expression
sylanblrc (𝜑𝜃)

Proof of Theorem sylanblrc
StepHypRef Expression
1 sylanblrc.1 . 2 (𝜑𝜓)
2 sylanblrc.2 . . 3 𝜒
32a1i 11 . 2 (𝜑𝜒)
4 sylanblrc.3 . 2 (𝜃 ↔ (𝜓𝜒))
51, 3, 4sylanbrc 584 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  fntp  6566  foimacnv  6805  respreima  7020  fpr  7104  fnprb  7162  curry1  8040  fnwelem  8067  frrlem12  8232  wfrlem13OLD  8271  tfrlem10  8337  oawordeulem  8505  oelim2  8546  oaabs2  8599  omabs  8601  ssdomg  8946  limenpsi  9102  dffi2  9367  gruina  10762  recmulnq  10908  reclem2pr  10992  climeu  15446  cosmul  16063  2ebits  16335  algcvgblem  16461  ismgmid  18528  mndideu  18575  ga0  19086  efgs1  19525  distopon  22370  dfac14  22992  ptcmplem5  23430  sszcld  24203  itg11  25078  axlowdimlem13  27952  nbusgredgeu  28363  1trld  29135  cycpmconjslem1  32059  1stmbfm  32924  2ndmbfm  32925  bnj150  33552  f1resfz0f1d  33768  satfrel  34025  satf0n0  34036  bj-projval  35517  exidu1  36365  rngoideu  36412  refrelressn  37036  rfcnpre1  43316  fundcmpsurinjlem2  45681
  Copyright terms: Public domain W3C validator