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

Theorem sylan9 689
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  1995  ax9  2002  rspc2  3318  rspc3v  3323  trintssOLD  4768  copsexg  4954  chfnrn  6326  fvcofneq  6365  ffnfv  6386  f1elima  6517  onint  6992  peano5  7086  f1oweALT  7149  smoel2  7457  pssnn  8175  fiint  8234  dffi2  8326  alephnbtwn  8891  cfcof  9093  zorn2lem7  9321  suplem1pr  9871  addsrpr  9893  mulsrpr  9894  cau3lem  14088  divalglem8  15117  efgi  18126  elfrlmbasn0  20100  locfincmp  21323  tx1stc  21447  fbunfip  21667  filuni  21683  ufileu  21717  rescncf  22694  shmodsi  28232  spanuni  28387  spansneleq  28413  mdi  29138  dmdi  29145  dmdi4  29150  funimass4f  29421  bj-ax89  32651  wl-ax8clv1  33358  wl-ax8clv2  33361  poimirlem32  33421  ffnafv  41020
  Copyright terms: Public domain W3C validator