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

Theorem sylan9 508
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 407 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  ax8  2112  ax9  2120  rspc2  3589  rspc2v  3591  rspc3v  3594  rspc4v  3596  rspc8v  3597  copsexgw  5452  copsexg  5453  chfnrn  7004  fvcofneq  7048  ffnfv  7071  f1elima  7215  onint  7730  peano5  7835  peano5OLD  7836  f1oweALT  7910  smoel2  8314  pssnn  9119  php  9161  pssnnOLD  9216  fiint  9275  dffi2  9368  alephnbtwn  10016  cfcof  10219  zorn2lem7  10447  suplem1pr  10997  addsrpr  11020  mulsrpr  11021  cau3lem  15251  divalglem8  16293  efgi  19515  elfrlmbasn0  21206  locfincmp  22914  tx1stc  23038  fbunfip  23257  filuni  23273  ufileu  23307  rescncf  24297  shmodsi  30394  spanuni  30549  spansneleq  30575  mdi  31300  dmdi  31307  dmdi4  31312  funimass4f  31618  bj-ax89  35218  poimirlem32  36183  ffnafv  45523
  Copyright terms: Public domain W3C validator