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  511  19.38a  1846  ax13lem1  2373  ax13lem2  2375  axc11n  2425  reuss2  4201  reupick  4205  elinxp  5857  ordtr2  6210  suc11  6269  funimass4  6728  fliftfun  7072  omlimcl  8228  nneob  8303  rankwflemb  9288  cflm  9743  domtriomlem  9935  grothomex  10322  sup3  11668  caubnd  14801  fbflim2  22721  ellimc3  24623  usgruspgrb  27118  usgredgsscusgredg  27393  3cyclfrgrrn1  28214  dfon2lem6  33328  opnrebl2  34140  bj-nfimt  34446  axc11n11r  34492  bj-nnf-alrim  34564  stdpc5t  34630  wl-ax13lem1  35277  diaintclN  38684  dibintclN  38793  dihintcl  38970  pm11.71  41537  axc11next  41546  rrx2plord2  45586
  Copyright terms: Public domain W3C validator