MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl31anc Unicode version

Theorem syl31anc 1185
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
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1132 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 642 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl32anc  1190  smo11  6397  omeulem2  6597  oeeui  6616  oaabs2  6659  omabs  6661  omxpenlem  6979  map2xp  7047  mapdom2  7048  cantnflt  7389  cnfcom  7419  mapcdaen  7826  pwsdompw  7846  cofsmo  7911  fin1a2lem4  8045  ltmul12a  9628  lt2msq1  9655  ledivp1  9674  lemul1ad  9712  lemul2ad  9713  supmul1  9735  supmul  9738  rpnnen1lem3  10360  rpnnen1lem5  10362  lediv2ad  10428  xaddge0  10594  xadddi  10631  xadddi2  10633  flval3  10961  fseqsupubi  11056  expcan  11170  ltexp2  11171  ltexp2r  11174  expubnd  11178  ltexp2rd  11285  ltexp2d  11290  leexp2d  11291  expcand  11292  swrdid  11474  ccatswrd  11475  swrdccat2  11477  splfv1  11486  swrds1  11489  o1fsum  12287  mertenslem1  12356  eftlub  12405  rpnnen2lem4  12512  ruclem12  12535  dvdsadd  12583  3dvds  12607  divalgmod  12621  bitsmod  12643  bitsinv1lem  12648  bezoutlem4  12736  gcdeq  12747  rplpwr  12751  sqgcd  12753  rpmulgcd2  12800  isprm5  12807  divgcdodd  12814  rpdvds  12819  divnumden  12835  crt  12862  phimullem  12863  coprimeprodsq2  12879  pythagtriplem19  12902  pockthlem  12968  prmunb  12977  prmreclem3  12981  prmreclem6  12984  ramub  13076  ramz  13088  mndodcong  14873  odngen  14904  pgpfi  14932  pgpssslw  14941  sylow2blem3  14949  lsmless1  14986  lsmless2  14987  lsmless12  14988  lsmmod2  15001  pj1id  15024  odadd2  15157  gexexlem  15160  ablfacrplem  15316  ablfacrp  15317  ablfac1b  15321  ablfac1eu  15324  pgpfac1lem2  15326  lsmssspx  15857  lspsncv0  15915  coe1subfv  16359  znunit  16533  clsndisj  16828  rnelfm  17664  fmfnfmlem2  17666  fmfnfm  17669  flimss1  17684  isfcf  17745  xblss2  17974  stdbdxmet  18077  metcnpi3  18108  nmoi  18253  nmoi2  18255  nmoco  18262  blcvx  18320  icccmplem2  18344  icccmplem3  18345  reconnlem2  18348  xrge0gsumle  18354  metds0  18370  metdstri  18371  metdseq0  18374  lebnumlem3  18477  nmoleub2lem  18611  bcthlem5  18766  minveclem2  18806  minveclem3b  18808  minveclem4  18812  minveclem6  18814  icombl  18937  cncombf  19029  mbflimsup  19037  itg2monolem1  19121  itg2mono  19124  itg2cnlem1  19132  itg2cnlem2  19133  bddmulibl  19209  ellimc2  19243  cpnord  19300  cpnres  19302  dvmulbr  19304  dvcobr  19311  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  dvivthlem1  19371  lhop1lem  19376  lhop1  19377  dvfsumlem2  19390  itgsubstlem  19411  deg1add  19505  deg1sublt  19512  ply1remlem  19564  plyeq0lem  19608  taylthlem2  19769  ulmdvlem3  19795  abelthlem7  19830  pilem2  19844  pilem3  19845  pige3  19901  logccv  20026  cxpaddlelem  20107  cvxcl  20295  fsumharmonic  20321  ftalem5  20330  dvdsdivcl  20437  dvdsmulf1o  20450  bposlem1  20539  lgsqr  20601  lgsquad2lem2  20614  2sqlem8a  20626  2sqlem8  20627  dchrmusum2  20659  dchrvmasumiflem1  20666  dchrisum0flblem1  20673  dchrisum0lem1b  20680  pntlem3  20774  nmoub3i  21367  ubthlem3  21467  minvecolem2  21470  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  htthlem  21513  pjpjpre  22014  chscllem1  22232  chscllem2  22233  chscllem3  22234  cnlnadjlem2  22664  leopnmid  22734  ballotlemsgt1  23085  ballotlemsel1i  23087  snunioc  23282  esumcst  23451  esumpcvgval  23461  dya2iocbrsiga  23593  bayesth  23657  erdszelem8  23744  vdgrun  23908  vdgr1d  23909  vdgr1b  23910  vdgr1a  23912  br8  24184  axsegcon  24627  ax5seglem1  24628  ax5seglem2  24629  axlowdimlem6  24647  axeuclidlem  24662  axcontlem7  24670  axcontlem9  24672  axcontlem10  24673  supaddc  24995  supadd  24996  areacirclem3  25029  cmptdst  25671  cmptdst2  25674  limnumrr  25725  flfneic  25727  flfneicn  25728  idcatfun  26044  rocatval  26062  indcls2  26099  totbndbnd  26616  prdsbnd  26620  rrncmslem  26659  rrntotbnd  26663  isdrngo2  26692  mzpsubst  26929  rencldnfi  27007  irrapx1  27016  pellexlem3  27019  pellexlem5  27021  infmrgelbi  27066  pellqrex  27067  pellfundge  27070  rmspecfund  27097  congtr  27155  acongeq  27173  bezoutr  27175  jm2.20nn  27193  jm2.25lem1  27194  jm2.26  27198  expdiophlem1  27217  uvcvvcl2  27340  uvcvv1  27341  uvcvv0  27342  hbtlem2  27431  pmtrprfv  27499  lsatcmp  29815  lcvexchlem2  29847  lcvexchlem3  29848  ncvr1  30084  cvrletrN  30085  cvrnbtwn3  30088  cvrnrefN  30094  cvrcmp  30095  0ltat  30103  atnle0  30121  atlen0  30122  cvlcvr1  30151  cvrval3  30224  atle  30247  athgt  30267  1cvratex  30284  ps-2  30289  ps-2b  30293  llnnleat  30324  2atneat  30326  llnle  30329  atcvrlln  30331  llncmp  30333  2llnmat  30335  2at0mat0  30336  2atm  30338  ps-2c  30339  lplnle  30351  lplnnle2at  30352  llncvrlpln2  30368  llncvrlpln  30369  2lplnmN  30370  2llnmj  30371  2atmat  30372  lplncmp  30373  lplnexllnN  30375  2llnm2N  30379  2llnm4  30381  lvolnle3at  30393  4atlem3a  30408  4atlem3b  30409  4atlem10  30417  4atlem11  30420  4atlem12  30423  lplncvrlvol2  30426  lplncvrlvol  30427  lvolcmp  30428  2lplnm2N  30432  2lplnmj  30433  dalempjsen  30464  dalemcea  30471  dalem2  30472  dalemdea  30473  dalem9  30483  dalem16  30490  dalemcjden  30503  dalem21  30505  dalem23  30507  dalem39  30522  dalem54  30537  dalem60  30543  cdlemb  30605  elpadd2at  30617  paddasslem4  30634  paddasslem7  30637  paddasslem15  30645  paddasslem16  30646  pmodlem1  30657  pmodlem2  30658  llnexchb2  30680  pclfinclN  30761  osumcllem9N  30775  pmapojoinN  30779  pexmidN  30780  pl42lem1N  30790  lhp0lt  30814  lhpexle1  30819  lhpexle2lem  30820  lhpexle3lem  30822  lhprelat3N  30851  ltrnid  30946  trlval3  30998  arglem1N  31001  cdlemc5  31006  cdleme3b  31040  cdleme3c  31041  cdleme3h  31046  cdleme7e  31058  cdleme7ga  31059  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme22b  31152  cdlemefrs29clN  31210  cdlemefrs32fva  31211  cdlemeg46fvcl  31317  cdlemeg46c  31324  cdlemeg46fvaw  31327  cdlemeg46req  31340  cdleme48fgv  31349  cdlemf1  31372  cdlemg1cex  31399  cdlemg2dN  31401  cdlemg2ce  31403  cdlemg12e  31458  cdlemg35  31524  cdlemh  31628  tendocan  31635  cdlemk28-3  31719  tendoex  31786  dih1  32098  dihmeetlem9N  32127  dihlspsnssN  32144  dihlspsnat  32145  lcfrlem23  32377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator