Theorem syl31anc 1241

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 1177	. 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 978

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 980

This theorem is referenced by:  syl32anc  1246  stoic4b  1431  enq0tr  7408  ltmul12a  8790  lt2msq1  8815  ledivp1  8833  lemul1ad  8869  lemul2ad  8870  lediv2ad  9690  xaddge0  9849  difelfznle  10105  expubnd  10547  nn0leexp2  10659  expcanlem  10663  expcand  10665  xrmaxaddlem  11236  mertenslemi1  11511  eftlub  11666  dvdsadd  11811  divalgmod  11899  gcdzeq  11990  rplpwr  11995  sqgcd  11997  bezoutr  12000  rpmulgcd2  12062  rpdvds  12066  isprm5  12109  divgcdodd  12110  oddpwdclemxy  12136  divnumden  12163  crth  12191  phimullem  12192  coprimeprodsq2  12225  pythagtriplem19  12249  pclemub  12254  pcpre1  12259  pcidlem  12289  pockthlem  12321  prmunb  12327  xblss2ps  13484  xblss2  13485  metcnpi3  13597  limcimolemlt  13713  limccnp2cntop  13726  dvmulxxbr  13746  dvcoapbr  13751  2sqlem8a  14038  2sqlem8  14039