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  3590  rspc2v  3592  rspc3v  3595  rspc4v  3597  rspc8v  3598  copsexgw  5451  copsexg  5452  chfnrn  7003  fvcofneq  7047  ffnfv  7070  f1elima  7214  onint  7729  peano5  7834  peano5OLD  7835  f1oweALT  7909  smoel2  8313  pssnn  9118  php  9160  pssnnOLD  9215  fiint  9274  dffi2  9367  alephnbtwn  10015  cfcof  10218  zorn2lem7  10446  suplem1pr  10996  addsrpr  11019  mulsrpr  11020  cau3lem  15248  divalglem8  16290  efgi  19509  elfrlmbasn0  21192  locfincmp  22900  tx1stc  23024  fbunfip  23243  filuni  23259  ufileu  23293  rescncf  24283  shmodsi  30380  spanuni  30535  spansneleq  30561  mdi  31286  dmdi  31293  dmdi4  31298  funimass4f  31604  bj-ax89  35195  poimirlem32  36160  ffnafv  45493
  Copyright terms: Public domain W3C validator