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

Theorem sylanblrc 593
 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 586 1 (𝜑𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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  df-an 400 This theorem is referenced by:  fntp  6385  foimacnv  6607  respreima  6813  fpr  6893  fnprb  6948  curry1  7782  fnwelem  7808  wfrlem13  7950  tfrlem10  8006  oawordeulem  8163  oelim2  8204  oaabs2  8255  omabs  8257  ssdomg  8538  limenpsi  8676  dffi2  8871  gruina  10229  recmulnq  10375  reclem2pr  10459  climeu  14904  cosmul  15518  2ebits  15786  algcvgblem  15911  ismgmid  17867  mndideu  17914  ga0  18420  efgs1  18853  distopon  21602  dfac14  22223  ptcmplem5  22661  sszcld  23422  itg11  24295  axlowdimlem13  26748  nbusgredgeu  27156  1trld  27927  cycpmconjslem1  30846  1stmbfm  31628  2ndmbfm  31629  bnj150  32258  f1resfz0f1d  32471  satfrel  32724  satf0n0  32735  frrlem12  33244  bj-projval  34429  exidu1  35291  rngoideu  35338  rfcnpre1  41643  fundcmpsurinjlem2  43911
 Copyright terms: Public domain W3C validator