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

Theorem sylan9 690
 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 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 197  df-an 385 This theorem is referenced by:  ax8  2036  ax9  2043  rspc2  3351  rspc3v  3356  trintssOLD  4803  copsexg  4985  chfnrn  6368  fvcofneq  6407  ffnfv  6428  f1elima  6560  onint  7037  peano5  7131  f1oweALT  7194  smoel2  7505  pssnn  8219  fiint  8278  dffi2  8370  alephnbtwn  8932  cfcof  9134  zorn2lem7  9362  suplem1pr  9912  addsrpr  9934  mulsrpr  9935  cau3lem  14138  divalglem8  15170  efgi  18178  elfrlmbasn0  20154  locfincmp  21377  tx1stc  21501  fbunfip  21720  filuni  21736  ufileu  21770  rescncf  22747  shmodsi  28376  spanuni  28531  spansneleq  28557  mdi  29282  dmdi  29289  dmdi4  29294  funimass4f  29565  bj-ax89  32792  wl-ax8clv1  33508  wl-ax8clv2  33511  poimirlem32  33571  ffnafv  41572
 Copyright terms: Public domain W3C validator