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

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

Proof of Theorem sylanblc
StepHypRef Expression
1 sylanblc.1 . 2 (𝜑𝜓)
2 sylanblc.2 . 2 𝜒
3 sylanblc.3 . . 3 ((𝜓𝜒) ↔ 𝜃)
43biimpi 219 . 2 ((𝜓𝜒) → 𝜃)
51, 2, 4sylancl 589 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:  uniintsn  4888  xmulpnf1  12655  odd2np1  15681  eltg3i  21564  restntr  21785  cmpcld  22005  rnelfm  22556  ovolctb2  24094  iscgra  26601  isinag  26630  isleag  26639  iseqlg  26659  omlsilem  29183  noextendseq  33248  mblfinlem3  35054
 Copyright terms: Public domain W3C validator