Theorem sylan9r 469

Description: Nested syllogism inference conjoining dissimilar antecedents.

Hypotheses

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

Assertion

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

Proof of Theorem sylan9r

Step	Hyp	Ref	Expression
1		sylan9r.1	. . 3 |- (ph -> (ps -> ch))
2		sylan9r.2	. . 3 |- (th -> (ch -> ta))
3	1, 2	syl9r 58	. 2 |- (th -> (ph -> (ps -> ta)))
4	3	imp 350	1 |- ((th /\ ph) -> (ps -> ta))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sbequi 1228  a12studyALT 1379  ralxfrd 2897  limsssuc 3121  findsg 3157  tfinds 3161  tfindsg 3162  isofrlem 3901  f1oweALT 3906  oaordi 4180  sdomdomtr 4469  pssnn 4534  inf3lem2 4614  r1tr 4654  rankr1 4674  zorn2lem7 4794  unidom 4808  cardlim 4851  cardaleph 4885  cfub 4908  genpcd 5109  prlem934a 5137  xrub 6080  zeot 6199  dfuz 6202  uzwo4OLD 6210  iccsupr 6398  uzwo 6455  uzwoOLD 6456  bastop 7642  cncnp 7778  subgabl 8123  ocin 9169  spanun 9467  superpos 10281  nndivsub 10421

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