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 215 . 2 ((𝜓𝜒) → 𝜃)
51, 2, 4sylancl 586 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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 397
This theorem is referenced by:  uniintsn  4991  xmulpnf1  13252  odd2np1  16283  eltg3i  22463  restntr  22685  cmpcld  22905  rnelfm  23456  ovolctb2  25008  noextendseq  27167  iscgra  28057  isinag  28086  isleag  28095  iseqlg  28115  omlsilem  30650  mblfinlem3  36522
  Copyright terms: Public domain W3C validator