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-mp 5  ax-1 6  ax-2 7  ax-3 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  2966  sbciedf  3082  pw1equn  4332  pw1eqadj  4333  findsd  4411  nnsucelr  4429  ltfintri  4467  lenltfin  4470  ncfindi  4476  nnpw1ex  4485  tfin11  4494  tfindi  4497  tfinltfinlem1  4501  nnadjoinpw  4522  sfin112  4530  sfindbl  4531  sfintfin  4533  tfinnn  4535  sfinltfin  4536  sfin111  4537  vfinncvntnn  4549  vfinspsslem1  4551  vfinncsp  4555  phi11lem1  4596  fvopab4t  5386  composevalg  5818  trd  5922  pmfun  6016  elmapi  6017  ncdisjun  6137  ce2le  6234  lemuc1  6254  lecadd2  6267  spacind  6288  nchoicelem4  6293  nchoicelem6  6295  nchoicelem19  6308  nchoice  6309  dmfrec  6317