MPE Home 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