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  272  bija  385  equviniOLD  2480  equvel  2481  2eu6  2745  rgen2a  3223  rexraleqim  3626  elreldm  5792  tz6.12c  6686  onminex  7516  rntpos  7901  smores  7985  seqomlem2  8083  f1domg  8525  php  8698  fodomnum  9481  carduniima  9520  cardmin  9984  negn0  11067  sqrmo  14611  isch3  29027  cgrtriv  33520  wl-lem-moexsb  34914  grpomndo  35258  elghomlem2OLD  35269  tz6.12c-afv2  43724
  Copyright terms: Public domain W3C validator