Theorem syl13anc 1218

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 )
syl13anc.5	|- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )

Assertion

Ref	Expression
syl13anc	|- ( ph -> et )

Proof of Theorem syl13anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4		sylXanc.4	. . 3 |- ( ph -> ta )
5	2, 3, 4	3jca 1161	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
6		syl13anc.5	. 2 |- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )
7	1, 5, 6	syl2anc 408	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  syl23anc  1223  syl33anc  1231  caovassd  5930  caovcand  5933  caovordid  5937  caovordd  5939  caovdid  5946  caovdird  5949  swoer  6457  swoord1  6458  swoord2  6459  fimax2gtrilemstep  6794  iunfidisj  6834  ssfii  6862  suplub2ti  6888  prarloclem3  7310  fzosubel3  9978  seq3split  10257  seq3caopr  10261  zsumdc  11158  fsumiun  11251  divalglemex  11624  strle1g  12054  psmetsym  12503  psmettri  12504  psmetge0  12505  psmetres2  12507  xmetge0  12539  xmetsym  12542  xmettri  12546  metrtri  12551  xmetres2  12553  bldisj  12575  xblss2ps  12578  xblss2  12579  xmeter  12610  xmetxp  12681