Theorem syl31anc 1329

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.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		syl12anc.1	. . 3 |- ( ph -> ps )
2		syl12anc.2	. . 3 |- ( ph -> ch )
3		syl12anc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1242	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl22anc.4	. 2 |- ( ph -> ta )
6		syl31anc.5	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )
7	4, 5, 6	syl2anc 693	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl32anc  1334  stoic4b  1703  elovmpt3rab1  6893  smo11  7461  omeulem2  7663  oeeui  7682  oaabs2  7725  omabs  7727  omxpenlem  8061  map2xp  8130  mapdom2  8131  fsuppsssupp  8291  cantnflt  8569  cnfcom  8597  mapcdaen  9006  pwsdompw  9026  cofsmo  9091  fin1a2lem4  9225  ltmul12a  10879  lt2msq1  10907  ledivp1  10925  lemul1ad  10963  lemul2ad  10964  suprubd  10985  supaddc  10990  supadd  10991  supmul1  10992  supmul  10995  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  lediv2ad  11894  xaddge0  12088  xadddi  12125  xadddi2  12127  supicc  12320  supiccub  12321  supicclub  12322  difelfznle  12453  flval3  12616  expcan  12913  ltexp2  12914  ltexp2r  12917  expubnd  12921  ltexp2rd  13033  ltexp2d  13038  leexp2d  13039  expcand  13040  swrdid  13428  swrd0fv  13439  swrds1  13451  ccatswrd  13456  swrdccat2  13458  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12lem3  13490  splfv1  13506  cshwidxmod  13549  wrdl3s3  13705  o1fsum  14545  mertenslem1  14616  eftlub  14839  rpnnen2lem4  14946  ruclem12  14970  dvdsadd  15024  3dvds  15052  3dvdsOLD  15053  divalgmod  15129  divalgmodOLD  15130  bitsmod  15158  bitsinv1lem  15163  bezoutlem4  15259  gcdzeq  15271  rplpwr  15276  sqgcd  15278  bezoutr  15281  rpmulgcd2  15370  rpdvds  15374  coprmproddvdslem  15376  isprm5  15419  divgcdodd  15422  divnumden  15456  crth  15483  phimullem  15484  modprm0  15510  modprmn0modprm0  15512  coprimeprodsq2  15514  pythagtriplem19  15538  pockthlem  15609  prmunb  15618  prmreclem3  15622  prmreclem6  15625  ramub  15717  ramz  15729  pmtrprfv  17873  pmtrprfv3  17874  mndodcong  17961  odngen  17992  pgpfi  18020  pgpssslw  18029  sylow2blem3  18037  lsmless1  18074  lsmless2  18075  lsmless12  18076  lsmmod2  18089  pj1id  18112  odadd2  18252  gexexlem  18255  ablfacrplem  18464  ablfacrp  18465  ablfac1b  18469  ablfac1eu  18472  pgpfac1lem2  18474  kerf1hrm  18743  lsmssspx  19088  lspsncv0  19146  coe1subfv  19636  coe1fzgsumdlem  19671  znunit  19912  uvcvvcl2  20127  uvcvv1  20128  uvcvv0  20129  scmate  20316  mdetunilem2  20419  pmatcoe1fsupp  20506  mat2pmatlin  20540  decpmatmullem  20576  pmatcollpw1lem1  20579  pmatcollpw1lem2  20580  pm2mpghm  20621  chpscmat  20647  chp0mat  20651  chpidmat  20652  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  clsndisj  20879  neiptopnei  20936  rnelfm  21757  fmfnfmlem2  21759  fmfnfm  21762  flimss1  21777  isfcf  21838  cnextfun  21868  cnextfvval  21869  cnextf  21870  cnextcn  21871  cnextfres1  21872  ustuqtop1  22045  utopsnneiplem  22051  xblss2ps  22206  xblss2  22207  stdbdxmet  22320  metcnpi3  22351  metustexhalf  22361  nmoi  22532  nmoi2  22534  nmoco  22541  blcvx  22601  icccmplem2  22626  icccmplem3  22627  reconnlem2  22630  xrge0gsumle  22636  metds0  22653  metdstri  22654  metdseq0  22657  lebnumlem3  22762  nmoleub2lem  22914  bcthlem5  23125  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem6  23205  icombl  23332  cncombf  23425  mbflimsup  23433  itg2monolem1  23517  itg2mono  23520  itg2cnlem1  23528  itg2cnlem2  23529  bddmulibl  23605  ellimc2  23641  cpnord  23698  cpnres  23700  dvmulbr  23702  dvcobr  23709  dvlipcn  23757  dvlip2  23758  c1liplem1  23759  dvivthlem1  23771  lhop1lem  23776  lhop1  23777  dvfsumlem2  23790  itgsubstlem  23811  deg1add  23863  deg1sublt  23870  ply1remlem  23922  plyeq0lem  23966  taylthlem2  24128  ulmdvlem3  24156  abelthlem7  24192  pilem2  24206  pilem3  24207  pige3  24269  logccv  24409  cxpaddlelem  24492  cvxcl  24711  fsumharmonic  24738  ftalem5  24803  dvdsmulf1o  24920  bposlem1  25009  lgsqr  25076  lgsquad2lem2  25110  2lgsoddprmlem1  25133  2sqlem8a  25150  2sqlem8  25151  dchrmusum2  25183  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0lem1b  25204  pntlem3  25298  tgdim01  25402  axsegcon  25807  ax5seglem1  25808  ax5seglem2  25809  axlowdimlem6  25827  axeuclidlem  25842  axcontlem7  25850  axcontlem9  25852  axcontlem10  25853  nbupgr  26240  nbumgrvtx  26242  cusgrsize2inds  26349  upgriswlk  26537  2pthnloop  26627  numclwwlkovf2exlem2  27212  numclwwlk2lem1  27235  frgrreg  27252  nmoub3i  27628  ubthlem3  27728  minvecolem2  27731  minvecolem4  27736  minvecolem5  27737  minvecolem6  27738  htthlem  27774  pjpjpre  28278  chscllem1  28496  chscllem2  28497  chscllem3  28498  cnlnadjlem2  28927  leopnmid  28997  br8d  29422  ogrpaddlt  29718  archirngz  29743  ornglmullt  29807  orngrmullt  29808  elrhmunit  29820  qqhval2lem  30025  qqhnm  30034  qqhucn  30036  esumcst  30125  esumpcvgval  30140  measunl  30279  dya2iocbrsiga  30337  dya2icobrsiga  30338  omssubadd  30362  inelcarsg  30373  carsgclctunlem2  30381  sibfof  30402  sitgaddlemb  30410  oddpwdc  30416  eulerpartlemgc  30424  bayesth  30501  ftc2re  30676  breprexplemc  30710  tgoldbachgt  30741  erdszelem8  31180  br8  31646  noetalem3  31865  noetalem5  31867  matunitlindflem2  33406  totbndbnd  33588  prdsbnd  33592  rrncmslem  33631  rrntotbnd  33635  isdrngo2  33757  lsatcmp  34290  lcvexchlem2  34322  lcvexchlem3  34323  ncvr1  34559  cvrletrN  34560  cvrnbtwn3  34563  cvrnrefN  34569  cvrcmp  34570  0ltat  34578  atnle0  34596  atlen0  34597  cvlcvr1  34626  cvrval3  34699  atle  34722  athgt  34742  1cvratex  34759  ps-2  34764  ps-2b  34768  llnnleat  34799  2atneat  34801  llnle  34804  atcvrlln  34806  llncmp  34808  2llnmat  34810  2at0mat0  34811  2atm  34813  ps-2c  34814  lplnle  34826  lplnnle2at  34827  llncvrlpln2  34843  llncvrlpln  34844  2lplnmN  34845  2llnmj  34846  2atmat  34847  lplncmp  34848  lplnexllnN  34850  2llnm2N  34854  2llnm4  34856  lvolnle3at  34868  4atlem3a  34883  4atlem3b  34884  4atlem10  34892  4atlem11  34895  4atlem12  34898  lplncvrlvol2  34901  lplncvrlvol  34902  lvolcmp  34903  2lplnm2N  34907  2lplnmj  34908  dalempjsen  34939  dalemcea  34946  dalem2  34947  dalemdea  34948  dalem9  34958  dalem16  34965  dalemcjden  34978  dalem21  34980  dalem23  34982  dalem39  34997  dalem54  35012  dalem60  35018  cdlemb  35080  elpadd2at  35092  paddasslem4  35109  paddasslem7  35112  paddasslem15  35120  paddasslem16  35121  pmodlem1  35132  pmodlem2  35133  llnexchb2  35155  pclfinclN  35236  osumcllem9N  35250  pmapojoinN  35254  pexmidN  35255  pl42lem1N  35265  lhp0lt  35289  lhpexle1  35294  lhpexle2lem  35295  lhpexle3lem  35297  lhprelat3N  35326  ltrnid  35421  trlval3  35474  arglem1N  35477  cdlemc5  35482  cdleme3b  35516  cdleme3c  35517  cdleme3h  35522  cdleme7e  35534  cdleme7ga  35535  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme22b  35629  cdlemefrs29clN  35687  cdlemefrs32fva  35688  cdlemeg46fvcl  35794  cdlemeg46c  35801  cdlemeg46fvaw  35804  cdlemeg46req  35817  cdleme48fgv  35826  cdlemf1  35849  cdlemg1cex  35876  cdlemg2dN  35878  cdlemg2ce  35880  cdlemg12e  35935  cdlemg35  36001  cdlemh  36105  tendocan  36112  cdlemk28-3  36196  tendoex  36263  dih1  36575  dihmeetlem9N  36604  dihlspsnssN  36621  dihlspsnat  36622  lcfrlem23  36854  mzpsubst  37311  rencldnfi  37385  irrapx1  37392  pellexlem3  37395  pellexlem5  37397  infmrgelbi  37442  pellqrex  37443  pellfundge  37446  rmspecfund  37474  congtr  37532  acongeq  37550  jm2.20nn  37564  jm2.25lem1  37565  jm2.26  37569  expdiophlem1  37588  hbtlem2  37694  suprleubrd  38466  suprlubrd  38470  suprnmpt  39355  wessf1ornlem  39371  mpct  39393  upbdrech  39519  ssfiunibd  39523  uzfissfz  39542  xleadd2d  39543  suprltrp  39544  xleadd1d  39545  suprleubrnmpt  39649  iccintsng  39749  limcrecl  39861  fnlimfvre  39906  dvmulcncf  40140  dvdivcncf  40142  dvbdfbdioolem1  40143  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem1  40218  stoweidlem20  40237  stoweidlem24  40241  stoweidlem34  40251  stoweidlem45  40262  stoweidlem60  40277  fourierdlem20  40344  fourierdlem31  40355  fourierdlem38  40362  fourierdlem64  40387  fourierdlem79  40402  fourierdlem94  40417  fourierdlem113  40436  fouriersw  40448  fouriercn  40449  sge0isum  40644  hoicvr  40762  ovnsubaddlem2  40785  hoidmv1lelem1  40805  hoidmv1lelem3  40807  hoidmvlelem1  40809  hoidmvlelem4  40812  smflimlem2  40980  pfxfv  41399  fmtnof1  41447  lighneallem2  41523  upgrwlkupwlk  41721  lincresunit3  42270  elbigolo1  42351