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  7547  ltmul12a  8933  lt2msq1  8958  ledivp1  8976  lemul1ad  9012  lemul2ad  9013  lediv2ad  9841  xaddge0  10000  difelfznle  10257  expubnd  10741  nn0leexp2  10855  expcanlem  10860  expcand  10862  swrds1  11121  ccatswrd  11123  xrmaxaddlem  11571  mertenslemi1  11846  eftlub  12001  dvdsadd  12147  3dvds  12175  divalgmod  12238  bitsfzolem  12265  bitsfzo  12266  bitsmod  12267  bitsinv1lem  12272  gcdzeq  12343  rplpwr  12348  sqgcd  12350  bezoutr  12353  rpmulgcd2  12417  rpdvds  12421  isprm5  12464  divgcdodd  12465  oddpwdclemxy  12491  divnumden  12518  crth  12546  phimullem  12547  coprimeprodsq2  12581  pythagtriplem19  12605  pclemub  12610  pcpre1  12615  pcidlem  12646  pockthlem  12679  prmunb  12685  kerf1ghm  13610  elrhmunit  13939  rrgnz  14030  znunit  14421  xblss2ps  14876  xblss2  14877  metcnpi3  14989  limcimolemlt  15136  limccnp2cntop  15149  dvmulxxbr  15174  dvcoapbr  15179  ltexp2d  15414  mpodvdsmulf1o  15462  lgsquad2lem2  15559  2lgsoddprmlem1  15582  2sqlem8a  15599  2sqlem8  15600