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

Theorem syli 39
Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)
Hypotheses
Ref Expression
syli.1 (𝜓 → (𝜑𝜒))
syli.2 (𝜒 → (𝜑𝜃))
Assertion
Ref Expression
syli (𝜓 → (𝜑𝜃))

Proof of Theorem syli
StepHypRef Expression
1 syli.1 . 2 (𝜓 → (𝜑𝜒))
2 syli.2 . . 3 (𝜒 → (𝜑𝜃))
32com12 32 . 2 (𝜑 → (𝜒𝜃))
41, 3sylcom 30 1 (𝜓 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  ibd  258  bija  369  equvini  2492  equvel  2493  2eu6  2707  rgen2a  3126  rexraleqim  3478  elreldm  5486  tz6.12c  6352  onminex  7152  rntpos  7515  smores  7600  seqomlem2  7697  f1domg  8127  php  8298  fodomnum  9078  carduniima  9117  cardmin  9586  negn0  10659  sqrmo  14193  isch3  28431  cgrtriv  32439  wl-lem-moexsb  33677  grpomndo  33999  elghomlem2OLD  34010
  Copyright terms: Public domain W3C validator