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

Theorem sylan9 509
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 408 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ax8  2113  ax9  2121  rspc2  3587  rspc2v  3589  rspc3v  3592  copsexgw  5445  copsexg  5446  chfnrn  6995  fvcofneq  7038  ffnfv  7061  f1elima  7205  onint  7716  peano5  7821  peano5OLD  7822  f1oweALT  7896  smoel2  8277  pssnn  9046  php  9088  pssnnOLD  9143  fiint  9202  dffi2  9293  alephnbtwn  9941  cfcof  10144  zorn2lem7  10372  suplem1pr  10922  addsrpr  10945  mulsrpr  10946  cau3lem  15175  divalglem8  16218  efgi  19436  elfrlmbasn0  21098  locfincmp  22805  tx1stc  22929  fbunfip  23148  filuni  23164  ufileu  23198  rescncf  24188  shmodsi  30136  spanuni  30291  spansneleq  30317  mdi  31042  dmdi  31049  dmdi4  31054  funimass4f  31355  bj-ax89  35073  poimirlem32  36041  ffnafv  45194
  Copyright terms: Public domain W3C validator