Theorem sylan9 517

Description: Nested syllogism inference conjoining dissimilar antecedents. (The proof was shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
sylan9.1	|- (ph -> (ps -> ch))
sylan9.2	|- (th -> (ch -> ta))

Assertion

Ref	Expression
sylan9	|- ((ph /\ th) -> (ps -> ta))

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 |- (ph -> (ps -> ch))
2		sylan9.2	. . 3 |- (th -> (ch -> ta))
3	1, 2	syl9 71	. 2 |- (ph -> (th -> (ps -> ta)))
4	3	imp 377	1 |- ((ph /\ th) -> (ps -> ta))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sbequi 1598  sbal1 1737  a12study 1769  rcla42v 2384  rcla43v 2386  moi 2436  trintss 3427  copsexg 3537  onfr 3702  onint 3876  limom 3967  peano5 3975  chfnrn 4775  ffnfv 4801  isotr 4874  isotrALT 4875  f1oweALT 4883  th3q 5376  pssnn 5628  fiint 5650  fodomfi 5656  r1tr 5765  zorn2lem7 5956  unidom 5970  alephnbtwn 6016  axacndlem4 6114  axacnd 6116  suppsr2 6375  supxrre 7292  seq1ublem 8163  clim2serz 8394  rescncf 8534  metelcls 9243  oprabco 10159  shmodsi 10995  spanuni 11100  spansneleq 11126  mdi 11867  dmdi 11874  dmdi4 11879  divalglem8 13703  mulgcdlem2 13757  trintssOLD 13795  axfelem17 14047  f1elima 15719  wofi 15770  frfi 15771  rrncms 16019  prtlem18 16279  prter1 16282

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain