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  1433  enq0tr  7435  ltmul12a  8819  lt2msq1  8844  ledivp1  8862  lemul1ad  8898  lemul2ad  8899  lediv2ad  9721  xaddge0  9880  difelfznle  10137  expubnd  10579  nn0leexp2  10692  expcanlem  10697  expcand  10699  xrmaxaddlem  11270  mertenslemi1  11545  eftlub  11700  dvdsadd  11845  divalgmod  11934  gcdzeq  12025  rplpwr  12030  sqgcd  12032  bezoutr  12035  rpmulgcd2  12097  rpdvds  12101  isprm5  12144  divgcdodd  12145  oddpwdclemxy  12171  divnumden  12198  crth  12226  phimullem  12227  coprimeprodsq2  12260  pythagtriplem19  12284  pclemub  12289  pcpre1  12294  pcidlem  12324  pockthlem  12356  prmunb  12362  xblss2ps  13943  xblss2  13944  metcnpi3  14056  limcimolemlt  14172  limccnp2cntop  14185  dvmulxxbr  14205  dvcoapbr  14210  2lgsoddprmlem1  14492  2sqlem8a  14508  2sqlem8  14509