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  268  bija  379  equvel  2449  2eu6  2645  rgen2a  3354  rexraleqim  3630  elreldm  5937  tz6.12cOLD  6923  onminex  7806  rntpos  8245  smores  8373  seqomlem2  8472  f1domg  8993  php  9238  phpOLD  9250  fodomnum  10087  carduniima  10126  cardmin  10594  negn0  11680  sqrmo  15242  isch3  31143  cgrtriv  35749  wl-lem-moexsb  37186  grpomndo  37499  elghomlem2OLD  37510  tz6.12c-afv2  46765
  Copyright terms: Public domain W3C validator