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

Theorem sylan9 687
 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 75 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43imp 444 1 ((𝜑𝜃) → (𝜓𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  ax8  1983  ax9  1990  rspc2  3292  rspc3v  3296  trintss  4697  copsexg  4882  chfnrn  6236  fvcofneq  6275  ffnfv  6295  f1elima  6421  onint  6887  peano5  6981  f1oweALT  7043  smoel2  7347  pssnn  8063  fiint  8122  dffi2  8212  alephnbtwn  8777  cfcof  8979  zorn2lem7  9207  suplem1pr  9753  addsrpr  9775  mulsrpr  9776  cau3lem  13942  divalglem8  14961  efgi  17955  elfrlmbasn0  19925  locfincmp  21139  tx1stc  21263  fbunfip  21483  filuni  21499  ufileu  21533  rescncf  22508  shmodsi  27632  spanuni  27787  spansneleq  27813  mdi  28538  dmdi  28545  dmdi4  28550  funimass4f  28818  bj-ax89  31854  poimirlem32  32611  ffnafv  39900
 Copyright terms: Public domain W3C validator