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

Theorem sylan9 688
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
sylan9.1 (𝜑 → (𝜓𝜒))
sylan9.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
sylan9 ((𝜑𝜃) → (𝜓𝜏))

Proof of Theorem sylan9
StepHypRef Expression
1 sylan9.1 . . 3 (𝜑 → (𝜓𝜒))
2 sylan9.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2syl9 77 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43imp 445 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  ax8  1998  ax9  2005  rspc2  3310  rspc3v  3314  trintssOLD  4735  copsexg  4921  chfnrn  6285  fvcofneq  6324  ffnfv  6344  f1elima  6475  onint  6943  peano5  7037  f1oweALT  7100  smoel2  7406  pssnn  8123  fiint  8182  dffi2  8274  alephnbtwn  8839  cfcof  9041  zorn2lem7  9269  suplem1pr  9819  addsrpr  9841  mulsrpr  9842  cau3lem  14023  divalglem8  15042  efgi  18048  elfrlmbasn0  20020  locfincmp  21234  tx1stc  21358  fbunfip  21578  filuni  21594  ufileu  21628  rescncf  22603  shmodsi  28088  spanuni  28243  spansneleq  28269  mdi  28994  dmdi  29001  dmdi4  29006  funimass4f  29271  bj-ax89  32301  poimirlem32  33059  ffnafv  40542
  Copyright terms: Public domain W3C validator