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  503  19.38a  1938  ax13lem1  2391  ax13lem2  2393  axc11n  2447  sbequi  2506  reuss2  4136  reupick  4140  elinxp  5670  elresOLD  5672  ordtr2  6007  suc11  6066  funimass4  6494  fliftfun  6817  omlimcl  7925  nneob  7999  rankwflemb  8933  cflm  9387  domtriomlem  9579  grothomex  9966  sup3  11310  caubnd  14475  fbflim2  22151  ellimc3  24042  usgruspgrb  26480  usgredgsscusgredg  26757  3cyclfrgrrn1  27655  dfon2lem6  32220  opnrebl2  32843  bj-exlalrim  33122  bj-nfimt  33135  axc11n11r  33201  stdpc5t  33331  wl-ax13lem1  33827  diaintclN  37126  dibintclN  37235  dihintcl  37412  pm11.71  39430  axc11next  39439
  Copyright terms: Public domain W3C validator