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  260  bija  371  equvini  2504  equvel  2505  2eu6  2720  rgen2a  3163  rexraleqim  3520  elreldm  5549  tz6.12c  6431  onminex  7235  rntpos  7598  smores  7683  seqomlem2  7780  f1domg  8210  php  8381  fodomnum  9161  carduniima  9200  cardmin  9669  negn0  10742  sqrmo  14213  isch3  28424  cgrtriv  32428  wl-lem-moexsb  33662  grpomndo  33983  elghomlem2OLD  33994  tz6.12c-afv2  41829
  Copyright terms: Public domain W3C validator