Theorem sylan9 470

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 221

This theorem is referenced by:  sbequi 1265  sbal1 1385  a12study 1417  rcla42v 1926  rcla43v 1928  moi 1971  onfr 3014  onint 3152  limom 3233  peano5 3241  chfnrn 3916  ffnfv 3942  isotr 4011  isotrALT 4012  f1oweALT 4020  th3q 4458  pssnn 4681  fiint 4703  fodomfi 4709  r1tr 4800  zorn2lem7 4940  unidom 4954  alephnbtwn 5018  axacndlem4 5116  axacnd 5118  suppsr2 5377  supxrre 6251  seq1ublem 7114  clim2serz 7337  rescncf 7477  metelcls 8176  shmodsi 9638  spanuni 9743  spansneleq 9769  mdi 10503  dmdi 10510  dmdi4 10515  oprabco 11811  f1elima 11818  rrncms 12075

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 145  df-an 223

Copyright terms: Public domain