MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syli Structured version   Visualization version   GIF version

Theorem syli 38
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  257  bija  369  equvini  2334  equvel  2335  2eu6  2546  rgen2a  2960  rexraleqim  3299  elreldm  5271  tz6.12c  6123  onminex  6899  rntpos  7252  smores  7336  seqomlem2  7433  f1domg  7861  php  8029  fodomnum  8763  carduniima  8802  cardmin  9265  negn0  10338  sqrmo  13840  isch3  27482  cgrtriv  31279  wl-lem-moexsb  32529  grpomndo  32844  elghomlem2OLD  32855
  Copyright terms: Public domain W3C validator