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  261  bija  373  equviniOLD  2393  equvel  2394  2eu6  2690  rgen2a  3171  rexraleqim  3550  elreldm  5646  tz6.12c  6522  onminex  7337  rntpos  7707  smores  7792  seqomlem2  7889  f1domg  8325  php  8496  fodomnum  9276  carduniima  9315  cardmin  9783  negn0  10869  sqrmo  14471  isch3  28813  cgrtriv  33017  wl-lem-moexsb  34278  grpomndo  34628  elghomlem2OLD  34639  tz6.12c-afv2  42877
  Copyright terms: Public domain W3C validator