Theorem syl3anc 1182

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	|- (ph -> ps)
sylXanc.2	|- (ph -> ch)
sylXanc.3	|- (ph -> th)
syl111anc.4	|- ((ps /\ ch /\ th) -> ta)

Assertion

Ref	Expression
syl3anc	|- (ph -> ta)

Proof of Theorem syl3anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- (ph -> ps)
2		sylXanc.2	. . 3 |- (ph -> ch)
3		sylXanc.3	. . 3 |- (ph -> th)
4	1, 2, 3	3jca 1132	. 2 |- (ph -> (ps /\ ch /\ th))
5		syl111anc.4	. 2 |- ((ps /\ ch /\ th) -> ta)
6	4, 5	syl 15	1 |- (ph -> ta)

Syntax hints:   -> wi 4   /\ w3a 934

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936

This theorem is referenced by:  syl112anc  1186  syl121anc  1187  syl211anc  1188  syl113anc  1194  syl131anc  1195  syl311anc  1196  syld3an3  1227  3jaod  1246  mpd3an23  1279  rspc3ev  2965  sbciedf  3081  pw1equn  4331  pw1eqadj  4332  findsd  4410  nnsucelr  4428  ltfintri  4466  lenltfin  4469  ncfindi  4475  nnpw1ex  4484  tfin11  4493  tfindi  4496  tfinltfinlem1  4500  nnadjoinpw  4521  sfin112  4529  sfindbl  4530  sfintfin  4532  tfinnn  4534  sfinltfin  4535  sfin111  4536  vfinncvntnn  4548  vfinspsslem1  4550  vfinncsp  4554  phi11lem1  4595  fvopab4t  5385  composevalg  5817  trd  5921  pmfun  6015  elmapi  6016  ncdisjun  6136  ce2le  6233  lemuc1  6253  lecadd2  6266  spacind  6287  nchoicelem4  6292  nchoicelem6  6294  nchoicelem19  6307  nchoice  6308  dmfrec  6316