Theorem syl31anc 1281

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 1208	. 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 415	1 |- ( ph -> et )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl32anc  1286  stoic4b  1482  mapfi  7261  enq0tr  7801  ltmul12a  9190  lt2msq1  9215  ledivp1  9233  lemul1ad  9269  lemul2ad  9270  lediv2ad  10120  xaddge0  10280  difelfznle  10542  expubnd  11033  nn0leexp2  11148  expcanlem  11153  expcand  11155  hashmap  11268  swrds1  11440  ccatswrd  11442  pfxfv  11456  swrdccatin1  11497  pfxccatin12lem3  11504  xrmaxaddlem  12026  mertenslemi1  12302  eftlub  12457  dvdsadd  12603  3dvds  12631  divalgmod  12694  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitsinv1lem  12728  gcdzeq  12799  rplpwr  12804  sqgcd  12806  bezoutr  12809  rpmulgcd2  12873  rpdvds  12877  isprm5  12920  divgcdodd  12921  oddpwdclemxy  12947  divnumden  12974  crth  13002  phimullem  13003  coprimeprodsq2  13037  pythagtriplem19  13061  pclemub  13066  pcpre1  13071  pcidlem  13102  pockthlem  13135  prmunb  13141  kerf1ghm  14077  elrhmunit  14484  rrgnz  14577  znunit  14994  xblss2ps  15505  xblss2  15506  metcnpi3  15618  limcimolemlt  15765  limccnp2cntop  15778  dvmulxxbr  15803  dvcoapbr  15808  ltexp2d  16044  pellexlem3  16093  mpodvdsmulf1o  16104  lgsquad2lem2  16201  2lgsoddprmlem1  16224  2sqlem8a  16241  2sqlem8  16242