Theorem syl221anc 1289

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

Assertion

Ref	Expression
syl221anc	|- ( ph -> ze )

Proof of Theorem syl221anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. 2 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4		sylXanc.4	. . 3 |- ( ph -> ta )
5	3, 4	jca 306	. 2 |- ( ph -> ( th /\ ta ) )
6		sylXanc.5	. 2 |- ( ph -> et )
7		syl221anc.6	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ et ) -> ze )
8	1, 2, 5, 6, 7	syl211anc 1284	1 |- ( ph -> ze )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl222anc  1294  vtocldf  2874  dmdcanapd  9158  exprecap  11038  fzowrddc  11441  xrbdtri  12067  2strbasg  13533  2stropg  13534  fnpr2o  13719  cnptoprest  15465  blssps  15653  blss  15654  metequiv2  15722  xmettx  15736  edgstruct  16510  usgr2v1e2w  16692