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  7802  ltmul12a  9193  lt2msq1  9218  ledivp1  9236  lemul1ad  9272  lemul2ad  9273  lediv2ad  10131  xaddge0  10291  difelfznle  10553  expubnd  11048  nn0leexp2  11164  expcanlem  11169  expcand  11171  hashmap  11284  swrds1  11456  ccatswrd  11458  pfxfv  11472  swrdccatin1  11513  pfxccatin12lem3  11520  xrmaxaddlem  12045  mertenslemi1  12321  eftlub  12476  dvdsadd  12622  3dvds  12650  divalgmod  12713  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitsinv1lem  12747  gcdzeq  12818  rplpwr  12823  sqgcd  12825  bezoutr  12828  rpmulgcd2  12892  rpdvds  12896  isprm5  12940  divgcdodd  12941  nnmaxpwlemxy  12967  divnumden  12995  crth  13025  phimullem  13026  coprimeprodsq2  13060  pythagtriplem19  13084  pclemub  13089  pcpre1  13094  pcidlem  13125  pockthlem  13158  prmunb  13164  kerf1ghm  14130  elrhmunit  14568  rrgnz  14661  znunit  15078  xblss2ps  15596  xblss2  15597  metcnpi3  15709  limcimolemlt  15856  limccnp2cntop  15869  dvmulxxbr  15894  dvcoapbr  15899  ltexp2d  16139  pellexlem3  16192  mpodvdsmulf1o  16245  bposlem1  16272  lgsquad2lem2  16367  2lgsoddprmlem1  16390  2sqlem8a  16407  2sqlem8  16408