Theorem syl31anc 1252

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

Assertion

Ref	Expression
syl31anc	|- ( ph -> et )

Proof of Theorem syl31anc

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  syl32anc  1257  stoic4b  1444  enq0tr  7518  ltmul12a  8904  lt2msq1  8929  ledivp1  8947  lemul1ad  8983  lemul2ad  8984  lediv2ad  9811  xaddge0  9970  difelfznle  10227  expubnd  10705  nn0leexp2  10819  expcanlem  10824  expcand  10826  xrmaxaddlem  11442  mertenslemi1  11717  eftlub  11872  dvdsadd  12018  3dvds  12046  divalgmod  12109  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitsinv1lem  12143  gcdzeq  12214  rplpwr  12219  sqgcd  12221  bezoutr  12224  rpmulgcd2  12288  rpdvds  12292  isprm5  12335  divgcdodd  12336  oddpwdclemxy  12362  divnumden  12389  crth  12417  phimullem  12418  coprimeprodsq2  12452  pythagtriplem19  12476  pclemub  12481  pcpre1  12486  pcidlem  12517  pockthlem  12550  prmunb  12556  kerf1ghm  13480  elrhmunit  13809  rrgnz  13900  znunit  14291  xblss2ps  14724  xblss2  14725  metcnpi3  14837  limcimolemlt  14984  limccnp2cntop  14997  dvmulxxbr  15022  dvcoapbr  15027  ltexp2d  15262  mpodvdsmulf1o  15310  lgsquad2lem2  15407  2lgsoddprmlem1  15430  2sqlem8a  15447  2sqlem8  15448