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 )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

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 1011

This theorem is referenced by:  syl32anc  1286  stoic4b  1482  mapfi  7251  enq0tr  7791  ltmul12a  9180  lt2msq1  9205  ledivp1  9223  lemul1ad  9259  lemul2ad  9260  lediv2ad  10099  xaddge0  10259  difelfznle  10520  expubnd  11011  nn0leexp2  11126  expcanlem  11131  expcand  11133  hashmap  11246  swrds1  11418  ccatswrd  11420  pfxfv  11434  swrdccatin1  11475  pfxccatin12lem3  11482  xrmaxaddlem  12004  mertenslemi1  12280  eftlub  12435  dvdsadd  12581  3dvds  12609  divalgmod  12672  bitsfzolem  12699  bitsfzo  12700  bitsmod  12701  bitsinv1lem  12706  gcdzeq  12777  rplpwr  12782  sqgcd  12784  bezoutr  12787  rpmulgcd2  12851  rpdvds  12855  isprm5  12898  divgcdodd  12899  oddpwdclemxy  12925  divnumden  12952  crth  12980  phimullem  12981  coprimeprodsq2  13015  pythagtriplem19  13039  pclemub  13044  pcpre1  13049  pcidlem  13080  pockthlem  13113  prmunb  13119  kerf1ghm  14054  elrhmunit  14457  rrgnz  14550  znunit  14966  xblss2ps  15428  xblss2  15429  metcnpi3  15541  limcimolemlt  15688  limccnp2cntop  15701  dvmulxxbr  15726  dvcoapbr  15731  ltexp2d  15967  pellexlem3  16007  mpodvdsmulf1o  16018  lgsquad2lem2  16115  2lgsoddprmlem1  16138  2sqlem8a  16155  2sqlem8  16156