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  4990  xmulpnf1  13313  odd2np1  16375  eltg3i  22984  restntr  23206  cmpcld  23426  rnelfm  23977  ovolctb2  25541  noextendseq  27727  iscgra  28832  isinag  28861  isleag  28870  iseqlg  28890  omlsilem  31431  mblfinlem3  37646
  Copyright terms: Public domain W3C validator