Theorem syl22anc 1183

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)
sylXanc.4	|- (ph -> ta)
syl22anc.5	|- (((ps /\ ch) /\ (th /\ ta)) -> et)

Assertion

Ref	Expression
syl22anc	|- (ph -> et)

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- (ph -> ps)
2		sylXanc.2	. . 3 |- (ph -> ch)
3	1, 2	jca 518	. 2 |- (ph -> (ps /\ ch))
4		sylXanc.3	. 2 |- (ph -> th)
5		sylXanc.4	. 2 |- (ph -> ta)
6		syl22anc.5	. 2 |- (((ps /\ ch) /\ (th /\ ta)) -> et)
7	3, 4, 5, 6	syl12anc 1180	1 |- (ph -> et)

Syntax hints:   -> wi 4   /\ wa 358

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

This theorem is referenced by:  prepeano4  4452  preaddccan2  4456  ncfindi  4476  ncfinsn  4477  ncfineleq  4478  nnpw1ex  4485  tfin11  4494  tfinpw1  4495  ncfintfin  4496  tfindi  4497  tfinsuc  4499  evenodddisj  4517  sfin112  4530  vfintle  4547  vfinspsslem1  4551  vfinncsp  4555  enadj  6061  ncdisjun  6137  nntccl  6171  ceclnn1  6190  sbth  6207  tcncg  6225  cet  6235  spacis  6289  nchoicelem6  6295