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

Theorem sylan9 511
 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 410 1 ((𝜑𝜃) → (𝜓𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  ax8  2117  ax9  2125  rspc2  3549  rspc2v  3551  rspc3v  3554  copsexgw  5349  copsexg  5350  chfnrn  6810  fvcofneq  6850  ffnfv  6873  f1elima  7013  onint  7509  peano5  7604  f1oweALT  7677  smoel2  8010  pssnn  8738  pssnnOLD  8774  fiint  8828  dffi2  8920  alephnbtwn  9531  cfcof  9734  zorn2lem7  9962  suplem1pr  10512  addsrpr  10535  mulsrpr  10536  cau3lem  14762  divalglem8  15801  efgi  18912  elfrlmbasn0  20528  locfincmp  22226  tx1stc  22350  fbunfip  22569  filuni  22585  ufileu  22619  rescncf  23598  shmodsi  29271  spanuni  29426  spansneleq  29452  mdi  30177  dmdi  30184  dmdi4  30189  funimass4f  30494  bj-ax89  34405  poimirlem32  35369  ffnafv  44095
 Copyright terms: Public domain W3C validator