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

Theorem sylanblc 589
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 216 . 2 ((𝜓𝜒) → 𝜃)
51, 2, 4sylancl 586 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  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 207  df-an 396
This theorem is referenced by:  uniintsn  4985  xmulpnf1  13316  odd2np1  16378  eltg3i  22968  restntr  23190  cmpcld  23410  rnelfm  23961  ovolctb2  25527  noextendseq  27712  iscgra  28817  isinag  28846  isleag  28855  iseqlg  28875  omlsilem  31421  mblfinlem3  37666
  Copyright terms: Public domain W3C validator