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

Theorem syl9 75
 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 71 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  76  com23  84  sylan9  687  19.21t  2061  19.21t-1OLD  2200  ax13lem1  2236  ax13lem2  2284  axc11n  2295  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  sbequi  2363  reuss2  3866  reupick  3870  elres  5355  ordtr2  5685  suc11  5748  funimass4  6157  fliftfun  6462  omlimcl  7545  nneob  7619  rankwflemb  8539  cflm  8955  domtriomlem  9147  grothomex  9530  sup3  10859  caubnd  13946  fbflim2  21591  ellimc3  23449  3cyclfrgrarn1  26539  dfon2lem6  30937  opnrebl2  31486  axc11n11r  31860  stdpc5t  32002  bj-nfimt  32025  wl-ax13lem1  32466  diaintclN  35365  dibintclN  35474  dihintcl  35651  pm11.71  37619  axc11next  37629  usgruspgrb  40411  usgredgsscusgredg  40675  3cyclfrgrrn1  41455
 Copyright terms: Public domain W3C validator