Theorem syl31anc 1274

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 1201	. 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 1002

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 1004

This theorem is referenced by:  syl32anc  1279  stoic4b  1475  enq0tr  7632  ltmul12a  9018  lt2msq1  9043  ledivp1  9061  lemul1ad  9097  lemul2ad  9098  lediv2ad  9927  xaddge0  10086  difelfznle  10343  expubnd  10830  nn0leexp2  10944  expcanlem  10949  expcand  10951  swrds1  11215  ccatswrd  11217  pfxfv  11231  swrdccatin1  11272  pfxccatin12lem3  11279  xrmaxaddlem  11786  mertenslemi1  12061  eftlub  12216  dvdsadd  12362  3dvds  12390  divalgmod  12453  bitsfzolem  12480  bitsfzo  12481  bitsmod  12482  bitsinv1lem  12487  gcdzeq  12558  rplpwr  12563  sqgcd  12565  bezoutr  12568  rpmulgcd2  12632  rpdvds  12636  isprm5  12679  divgcdodd  12680  oddpwdclemxy  12706  divnumden  12733  crth  12761  phimullem  12762  coprimeprodsq2  12796  pythagtriplem19  12820  pclemub  12825  pcpre1  12830  pcidlem  12861  pockthlem  12894  prmunb  12900  kerf1ghm  13826  elrhmunit  14156  rrgnz  14247  znunit  14638  xblss2ps  15093  xblss2  15094  metcnpi3  15206  limcimolemlt  15353  limccnp2cntop  15366  dvmulxxbr  15391  dvcoapbr  15396  ltexp2d  15631  mpodvdsmulf1o  15679  lgsquad2lem2  15776  2lgsoddprmlem1  15799  2sqlem8a  15816  2sqlem8  15817