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

Theorem sylan9 503
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 395 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 198  df-an 385
This theorem is referenced by:  ax8  2161  ax9  2168  rspc2  3471  rspc3v  3476  copsexg  5110  chfnrn  6517  fvcofneq  6556  ffnfv  6577  f1elima  6711  onint  7192  peano5  7286  f1oweALT  7349  smoel2  7663  pssnn  8384  fiint  8443  dffi2  8535  alephnbtwn  9144  cfcof  9348  zorn2lem7  9576  suplem1pr  10126  addsrpr  10148  mulsrpr  10149  cau3lem  14380  divalglem8  15406  efgi  18397  elfrlmbasn0  20381  locfincmp  21608  tx1stc  21732  fbunfip  21951  filuni  21967  ufileu  22001  rescncf  22978  shmodsi  28638  spanuni  28793  spansneleq  28819  mdi  29544  dmdi  29551  dmdi4  29556  funimass4f  29821  bj-ax89  33034  wl-ax8clv1  33734  wl-ax8clv2  33737  poimirlem32  33797  ffnafv  41851
  Copyright terms: Public domain W3C validator