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  13642  psdmul  22188  efrlim  27027  addsval  28010  mulscan2d  28220  dvdsruasso  33393  ssdifidlprm  33466  fsuppssind  42580  tfsconcat0i  43335  oadif1lem  43369  oadif1  43370  reabsifneg  43622  natglobalincr  46831  f1cof1b  47027  isubgr3stgrlem6  47874  prsthinc  48855
  Copyright terms: Public domain W3C validator