Theorem syl31anc 1253

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 1180	. 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 981

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 983

This theorem is referenced by:  syl32anc  1258  stoic4b  1453  enq0tr  7582  ltmul12a  8968  lt2msq1  8993  ledivp1  9011  lemul1ad  9047  lemul2ad  9048  lediv2ad  9876  xaddge0  10035  difelfznle  10292  expubnd  10778  nn0leexp2  10892  expcanlem  10897  expcand  10899  swrds1  11159  ccatswrd  11161  pfxfv  11175  swrdccatin1  11216  pfxccatin12lem3  11223  xrmaxaddlem  11686  mertenslemi1  11961  eftlub  12116  dvdsadd  12262  3dvds  12290  divalgmod  12353  bitsfzolem  12380  bitsfzo  12381  bitsmod  12382  bitsinv1lem  12387  gcdzeq  12458  rplpwr  12463  sqgcd  12465  bezoutr  12468  rpmulgcd2  12532  rpdvds  12536  isprm5  12579  divgcdodd  12580  oddpwdclemxy  12606  divnumden  12633  crth  12661  phimullem  12662  coprimeprodsq2  12696  pythagtriplem19  12720  pclemub  12725  pcpre1  12730  pcidlem  12761  pockthlem  12794  prmunb  12800  kerf1ghm  13725  elrhmunit  14054  rrgnz  14145  znunit  14536  xblss2ps  14991  xblss2  14992  metcnpi3  15104  limcimolemlt  15251  limccnp2cntop  15264  dvmulxxbr  15289  dvcoapbr  15294  ltexp2d  15529  mpodvdsmulf1o  15577  lgsquad2lem2  15674  2lgsoddprmlem1  15697  2sqlem8a  15714  2sqlem8  15715