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  5923  caovcand  5926  caovordid  5930  caovordd  5932  caovdid  5939  caovdird  5942  swoer  6450  swoord1  6451  swoord2  6452  fimax2gtrilemstep  6787  iunfidisj  6827  ssfii  6855  suplub2ti  6881  prarloclem3  7298  fzosubel3  9966  seq3split  10245  seq3caopr  10249  zsumdc  11146  fsumiun  11239  divalglemex  11608  strle1g  12038  psmetsym  12487  psmettri  12488  psmetge0  12489  psmetres2  12491  xmetge0  12523  xmetsym  12526  xmettri  12530  metrtri  12535  xmetres2  12537  bldisj  12559  xblss2ps  12562  xblss2  12563  xmeter  12594  xmetxp  12665