Theorem syl13anc 1230

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 1167	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
6		syl13anc.5	. 2 |- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )
7	1, 5, 6	syl2anc 409	1 |- ( ph -> et )

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

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 970

This theorem is referenced by:  syl23anc  1235  syl33anc  1243  caovassd  6001  caovcand  6004  caovordid  6008  caovordd  6010  caovdid  6017  caovdird  6020  swoer  6529  swoord1  6530  swoord2  6531  fimax2gtrilemstep  6866  iunfidisj  6911  ssfii  6939  suplub2ti  6966  prarloclem3  7438  fzosubel3  10131  seq3split  10414  seq3caopr  10418  zsumdc  11325  fsumiun  11418  divalglemex  11859  pcgcd1  12259  strle1g  12485  psmetsym  12969  psmettri  12970  psmetge0  12971  psmetres2  12973  xmetge0  13005  xmetsym  13008  xmettri  13012  metrtri  13017  xmetres2  13019  bldisj  13041  xblss2ps  13044  xblss2  13045  xmeter  13076  xmetxp  13147