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

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

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

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

This theorem is referenced by:  syl23anc  1188  syl33anc  1196  caovassd  5842  caovcand  5845  caovordid  5849  caovordd  5851  caovdid  5858  caovdird  5861  swoer  6360  swoord1  6361  swoord2  6362  fimax2gtrilemstep  6696  iunfidisj  6735  suplub2ti  6776  prarloclem3  7153  fzosubel3  9756  seq3split  10045  seq3caopr  10049  zsumdc  10943  fsumiun  11036  divalglemex  11365  strle1g  11749  psmetsym  12131  psmettri  12132  psmetge0  12133  psmetres2  12135  xmetge0  12167  xmetsym  12170  xmettri  12174  metrtri  12179  xmetres2  12181  bldisj  12203  xblss2ps  12206  xblss2  12207  xmeter  12238