Theorem syl31anc 1236

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 1172	. 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 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:  syl32anc  1241  stoic4b  1426  enq0tr  7396  ltmul12a  8776  lt2msq1  8801  ledivp1  8819  lemul1ad  8855  lemul2ad  8856  lediv2ad  9676  xaddge0  9835  difelfznle  10091  expubnd  10533  nn0leexp2  10645  expcanlem  10649  expcand  10651  xrmaxaddlem  11223  mertenslemi1  11498  eftlub  11653  dvdsadd  11798  divalgmod  11886  gcdzeq  11977  rplpwr  11982  sqgcd  11984  bezoutr  11987  rpmulgcd2  12049  rpdvds  12053  isprm5  12096  divgcdodd  12097  oddpwdclemxy  12123  divnumden  12150  crth  12178  phimullem  12179  coprimeprodsq2  12212  pythagtriplem19  12236  pclemub  12241  pcpre1  12246  pcidlem  12276  pockthlem  12308  prmunb  12314  xblss2ps  13198  xblss2  13199  metcnpi3  13311  limcimolemlt  13427  limccnp2cntop  13440  dvmulxxbr  13460  dvcoapbr  13465  2sqlem8a  13752  2sqlem8  13753