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

Theorem sylbida 592
Description: A syllogism deduction. (Contributed by SN, 16-Jul-2024.)
Hypotheses
Ref Expression
sylbida.1 (𝜑 → (𝜓𝜒))
sylbida.2 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
sylbida ((𝜑𝜓) → 𝜃)

Proof of Theorem sylbida
StepHypRef Expression
1 sylbida.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpa 476 . 2 ((𝜑𝜓) → 𝜒)
3 sylbida.2 . 2 ((𝜑𝜒) → 𝜃)
42, 3syldan 591 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:  fzdif1  13645  psdmul  22170  efrlim  27012  addsval  27995  mulscan2d  28205  dvdsruasso  33413  ssdifidlprm  33486  fsuppssind  42603  tfsconcat0i  43358  oadif1lem  43392  oadif1  43393  reabsifneg  43645  natglobalincr  46892  f1cof1b  47089  isubgr3stgrlem6  47938  prsthinc  49111
  Copyright terms: Public domain W3C validator