Theorem syl31anc 1277

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 1204	. 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 1005

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 1007

This theorem is referenced by:  syl32anc  1282  stoic4b  1478  enq0tr  7697  ltmul12a  9082  lt2msq1  9107  ledivp1  9125  lemul1ad  9161  lemul2ad  9162  lediv2ad  9998  xaddge0  10157  difelfznle  10415  expubnd  10904  nn0leexp2  11018  expcanlem  11023  expcand  11025  swrds1  11298  ccatswrd  11300  pfxfv  11314  swrdccatin1  11355  pfxccatin12lem3  11362  xrmaxaddlem  11883  mertenslemi1  12159  eftlub  12314  dvdsadd  12460  3dvds  12488  divalgmod  12551  bitsfzolem  12578  bitsfzo  12579  bitsmod  12580  bitsinv1lem  12585  gcdzeq  12656  rplpwr  12661  sqgcd  12663  bezoutr  12666  rpmulgcd2  12730  rpdvds  12734  isprm5  12777  divgcdodd  12778  oddpwdclemxy  12804  divnumden  12831  crth  12859  phimullem  12860  coprimeprodsq2  12894  pythagtriplem19  12918  pclemub  12923  pcpre1  12928  pcidlem  12959  pockthlem  12992  prmunb  12998  kerf1ghm  13924  elrhmunit  14255  rrgnz  14347  znunit  14738  xblss2ps  15198  xblss2  15199  metcnpi3  15311  limcimolemlt  15458  limccnp2cntop  15471  dvmulxxbr  15496  dvcoapbr  15501  ltexp2d  15736  pellexlem3  15776  mpodvdsmulf1o  15787  lgsquad2lem2  15884  2lgsoddprmlem1  15907  2sqlem8a  15924  2sqlem8  15925