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 1223  sbal1 1341  a12study 1371  rcla42v 1871  rcla43v 1873  moi 1915  onfr 2976  onint 2996  limom 3136  peano5 3143  chfnrn 3787  ffnfv 3813  isotr 3882  isotrALT 3883  f1oweALT 3891  th3q 4301  pssnn 4513  fiint 4534  fodomfi 4540  r1tr 4626  zorn2lem7 4766  unidom 4780  alephnbtwn 4840  axacndlem4 4934  axacnd 4936  suppsr2 5195  supxrre 6030  seq1ublem 6848  clim2serzt 7070  rescncf 7207  metelcls 7900  shmods 9277  spanun 9382  spansneleq 9409  spansneleqOLD 9410  mdit 10132  dmdit 10139  dmdi4 10143

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