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

Theorem sylan9 491
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 393 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 197  df-an 383
This theorem is referenced by:  ax8  2150  ax9  2157  rspc2  3468  rspc3v  3473  trintssOLD  4901  copsexg  5083  chfnrn  6471  fvcofneq  6510  ffnfv  6530  f1elima  6662  onint  7141  peano5  7235  f1oweALT  7298  smoel2  7612  pssnn  8333  fiint  8392  dffi2  8484  alephnbtwn  9093  cfcof  9297  zorn2lem7  9525  suplem1pr  10075  addsrpr  10097  mulsrpr  10098  cau3lem  14301  divalglem8  15330  efgi  18338  elfrlmbasn0  20322  locfincmp  21549  tx1stc  21673  fbunfip  21892  filuni  21908  ufileu  21942  rescncf  22919  shmodsi  28582  spanuni  28737  spansneleq  28763  mdi  29488  dmdi  29495  dmdi4  29500  funimass4f  29771  bj-ax89  32998  wl-ax8clv1  33704  wl-ax8clv2  33707  poimirlem32  33767  ffnafv  41765
  Copyright terms: Public domain W3C validator