Theorem syl13anc 1235

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 1172	. 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 973

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 975

This theorem is referenced by:  syl23anc  1240  syl33anc  1248  caovassd  6012  caovcand  6015  caovordid  6019  caovordd  6021  caovdid  6028  caovdird  6031  swoer  6541  swoord1  6542  swoord2  6543  fimax2gtrilemstep  6878  iunfidisj  6923  ssfii  6951  suplub2ti  6978  prarloclem3  7459  fzosubel3  10152  seq3split  10435  seq3caopr  10439  zsumdc  11347  fsumiun  11440  divalglemex  11881  pcgcd1  12281  strle1g  12508  mnd32g  12663  mnd12g  12664  mnd4g  12665  ismndd  12673  mndinvmod  12678  grpasscan2  12763  grpidrcan  12764  grpidlcan  12765  grpinvinv  12766  psmetsym  13123  psmettri  13124  psmetge0  13125  psmetres2  13127  xmetge0  13159  xmetsym  13162  xmettri  13166  metrtri  13171  xmetres2  13173  bldisj  13195  xblss2ps  13198  xblss2  13199  xmeter  13230  xmetxp  13301