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  508  19.38a  1842  ax13lem1  2374  ax13lem2  2376  axc11n  2426  reuss2  4249  reupick  4252  elinxp  5929  ordtr2  6310  suc11  6369  funimass4  6834  fliftfun  7183  omlimcl  8409  nneob  8486  rankwflemb  9551  cflm  10006  domtriomlem  10198  grothomex  10585  sup3  11932  caubnd  15070  fbflim2  23128  ellimc3  25043  usgruspgrb  27551  usgredgsscusgredg  27826  3cyclfrgrrn1  28649  dfon2lem6  33764  opnrebl2  34510  bj-nfimt  34819  axc11n11r  34865  bj-nnf-alrim  34937  stdpc5t  35010  wl-ax13lem1  35665  diaintclN  39072  dibintclN  39181  dihintcl  39358  pm11.71  42015  axc11next  42024  rrx2plord2  46068
  Copyright terms: Public domain W3C validator