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

Theorem syl9 77
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Hypotheses
Ref Expression
syl9.1 (𝜑 → (𝜓𝜒))
syl9.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
syl9 (𝜑 → (𝜃 → (𝜓𝜏)))

Proof of Theorem syl9
StepHypRef Expression
1 syl9.1 . 2 (𝜑 → (𝜓𝜒))
2 syl9.2 . . 3 (𝜃 → (𝜒𝜏))
32a1i 11 . 2 (𝜑 → (𝜃 → (𝜒𝜏)))
41, 3syl5d 73 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:  syl9r  78  com23  86  sylan9  499  19.21tOLDOLD  2241  19.21t-1OLD  2386  ax13lem1  2422  ax13lem2  2463  axc11n  2474  sbequi  2534  reuss2  4108  reupick  4112  elinxp  5637  elresOLD  5639  ordtr2  5981  suc11  6044  funimass4  6468  fliftfun  6786  omlimcl  7895  nneob  7969  rankwflemb  8903  cflm  9357  domtriomlem  9549  grothomex  9936  sup3  11265  caubnd  14321  fbflim2  21994  ellimc3  23857  usgruspgrb  26291  usgredgsscusgredg  26583  3cyclfrgrrn1  27460  dfon2lem6  32013  opnrebl2  32637  bj-nfimt  32932  axc11n11r  32988  stdpc5t  33127  wl-ax13lem1  33605  diaintclN  36839  dibintclN  36948  dihintcl  37125  pm11.71  39097  axc11next  39106
  Copyright terms: Public domain W3C validator