Theorem sylan9 468

Description: Nested syllogism inference conjoining dissimilar antecedents.

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	1	adantr 389	. 2 |- ((ph /\ th) -> (ps -> ch))
3		sylan9.2	. . 3 |- (th -> (ch -> ta))
4	3	adantl 388	. 2 |- ((ph /\ th) -> (ch -> ta))
5	2, 4	syld 27	1 |- ((ph /\ th) -> (ps -> ta))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sbequi 1226  sbal1 1344  a12study 1376  rcla42v 1876  rcla43v 1878  moi 1921  onfr 2981  onint 3001  limom 3141  peano5 3148  chfnrn 3793  ffnfv 3819  isotr 3888  isotrALT 3889  f1oweALT 3897  th3q 4307  pssnn 4519  fiint 4540  fodomfi 4546  r1tr 4634  zorn2lem7 4774  unidom 4788  alephnbtwn 4848  axacndlem4 4942  axacnd 4944  suppsr2 5203  supxrre 6038  seq1ublem 6856  clim2serzt 7078  rescncf 7215  metelcls 7916  shmods 9300  spanun 9405  spansneleq 9432  spansneleqOLD 9433  mdit 10160  dmdit 10167  dmdi4 10172

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 147  df-an 225

Copyright terms: Public domain