Theorem sylan9r 471

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 1230  a12studyALT 1381  ralxfrd 2903  limsssuc 3127  findsg 3163  tfinds 3167  tfindsg 3168  isofrlem 3907  f1oweALT 3912  oaordi 4186  sdomdomtr 4475  pssnn 4544  inf3lem2 4623  r1tr 4664  rankr1 4684  zorn2lem7 4804  unidom 4818  cardlim 4862  cardaleph 4896  cfub 4920  genpcd 5121  prlem934a 5149  xrub 6082  zeot 6201  dfuz 6204  uzwo4OLD 6212  iccsupr 6399  uzwo 6456  uzwoOLD 6457  bastop 7641  cncnp 7775  subgabl 8119  ocin 9164  spanun 9462  superpos 10276  nndivsub 10416

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