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  370  equvini  2345  equvel  2346  2eu6  2557  rgen2a  2972  rexraleqim  3316  elreldm  5315  tz6.12c  6175  onminex  6961  rntpos  7317  smores  7401  seqomlem2  7498  f1domg  7926  php  8095  fodomnum  8831  carduniima  8870  cardmin  9337  negn0  10410  sqrmo  13933  isch3  27965  cgrtriv  31778  wl-lem-moexsb  33009  grpomndo  33333  elghomlem2OLD  33344
  Copyright terms: Public domain W3C validator