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  269  bija  380  equvel  2461  2eu6  2657  rgen2a  3371  rexraleqim  3647  elreldm  5946  tz6.12cOLD  6933  onminex  7822  rntpos  8264  smores  8392  seqomlem2  8491  f1domg  9012  php  9247  phpOLD  9259  fodomnum  10097  carduniima  10136  cardmin  10604  negn0  11692  sqrmo  15290  isch3  31260  cgrtriv  36003  wl-lem-moexsb  37569  grpomndo  37882  elghomlem2OLD  37893  tz6.12c-afv2  47254
  Copyright terms: Public domain W3C validator