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

Theorem sylanblc 588
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 215 . 2 ((𝜓𝜒) → 𝜃)
51, 2, 4sylancl 585 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395
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 396
This theorem is referenced by:  uniintsn  4992  xmulpnf1  13258  odd2np1  16289  eltg3i  22685  restntr  22907  cmpcld  23127  rnelfm  23678  ovolctb2  25242  noextendseq  27403  iscgra  28324  isinag  28353  isleag  28362  iseqlg  28382  omlsilem  30919  mblfinlem3  36831
  Copyright terms: Public domain W3C validator