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  688  nfimt  1819  19.21tOLDOLD  2072  19.21t-1OLD  2210  ax13lem1  2246  ax13lem2  2294  axc11n  2305  axc11nOLD  2306  axc11nOLDOLD  2307  axc11nALT  2308  sbequi  2373  reuss2  3899  reupick  3903  elres  5423  ordtr2  5756  suc11  5819  funimass4  6234  fliftfun  6547  omlimcl  7643  nneob  7717  rankwflemb  8641  cflm  9057  domtriomlem  9249  grothomex  9636  sup3  10965  caubnd  14079  fbflim2  21762  ellimc3  23624  usgruspgrb  26057  usgredgsscusgredg  26336  3cyclfrgrrn1  27129  dfon2lem6  31667  opnrebl2  32291  axc11n11r  32648  stdpc5t  32789  wl-ax13lem1  33258  diaintclN  36166  dibintclN  36275  dihintcl  36452  pm11.71  38417  axc11next  38427
  Copyright terms: Public domain W3C validator