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

Theorem simp1l 1012
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1l  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 457 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 1009 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  simpl1l  1039  simpr1l  1045  simp11l  1099  simp21l  1105  simp31l  1111  funprg  5479  tfisi  6481  omeulem2  7034  uniinqs  7192  unxpdomlem3  7531  elfiun  7692  cantnffval  7881  tcrank  8103  cofsmo  8450  isfin2-2  8500  tskint  8964  tskun  8965  tskurn  8968  gruina  8997  dedekind  9545  dmdcan  10053  lt2msq1  10227  supmullem1  10308  supmul  10310  xaddass  11224  xaddass2  11225  xlt2add  11235  xmulasslem3  11261  xadddi2r  11273  iccsplit  11430  expaddzlem  11919  expaddz  11920  expmulz  11922  ccatopth2  12377  swrdccat3  12395  resqrcl  12755  limsupgle  12967  o1add  13103  o1mul  13104  o1sub  13105  bitsfzo  13643  sadfval  13660  smufval  13685  prmexpb  13815  4sqlem18  14035  vdwlem10  14063  fsets  14212  submre  14555  mrelatlub  15368  mndodcong  16057  subgabl  16332  gex2abl  16345  cntzsubr  16909  abvres  16936  lbsind2  17174  lspsneu  17216  lbsextlem2  17252  lbsextg  17255  lindfind2  18259  matrng  18342  maducoeval  18457  maducoeval2  18458  maduf  18459  madurid  18462  gsummatr01  18477  cramerimplem3  18503  cnprest  18905  hausnei2  18969  isreg2  18993  cmpcld  19017  llyrest  19101  nllyrest  19102  csdfil  19479  hausflimlem  19564  ssblps  20009  ssbl  20010  dvres2  21399  plyadd  21697  plymul  21698  coeeu  21705  vieta1  21790  aalioulem3  21812  aalioulem4  21813  cxpadd  22136  cxpsub  22139  mulcxp  22142  divcxp  22144  cxple2  22154  cxplt2  22155  cxpcn3lem  22197  angcan  22210  ang180lem5  22221  isosctrlem3  22230  logexprlim  22576  abvcxp  22876  padicabv  22891  brbtwn2  23163  ax5seglem6  23192  axcontlem4  23225  axcontlem8  23229  chscllem4  25055  ogrpinvlt  26199  poseq  27726  wsuclem  27774  nofulllem5  27859  ifscgr  28087  congtr  29320  fzmaxdif  29336  isnumbasgrplem2  29472  stoweidlem34  29841  stoweidlem59  29866  stirlinglem13  29893  clwwlknimp  30451  pmatcollpw1lem3  30910  lincscm  30976  lincext3  31002  el0ldep  31012  el0ldepsnzr  31013  lshpnelb  32641  lfl1  32727  lshpkrlem6  32772  lshpkrex  32775  hlrelat3  33068  atbtwnexOLDN  33103  atbtwnex  33104  3dim3  33125  3atlem5  33143  2llnmat  33180  lvolex3N  33194  lvolnle3at  33238  4atlem11  33265  4atlem12  33268  dalemccea  33339  cdlema2N  33448  paddasslem2  33477  atmod1i1m  33514  lhp2lt  33657  lhp0lt  33659  lhpj1  33678  lhpmcvr4N  33682  lhpelim  33693  lhpmod2i2  33694  lhpmod6i1  33695  cdlemb2  33697  lhple  33698  lhpat  33699  4atex  33732  4atex2-0aOLDN  33734  4atex3  33737  ldilco  33772  ltrncl  33781  ltrn11  33782  ltrnle  33785  ltrncnvleN  33786  ltrnm  33787  ltrnj  33788  ltrncvr  33789  ltrnatb  33793  ltrnel  33795  ltrncnvel  33798  ltrncnv  33802  ltrnmw  33807  trlval2  33819  trlcnv  33821  trljat1  33822  trljat2  33823  trl0  33826  ltrnnidn  33830  trlnidatb  33833  cdlemc1  33847  cdlemc2  33848  cdlemc5  33851  cdlemc6  33852  cdlemd3  33856  cdlemd6  33859  cdleme0aa  33866  cdleme0b  33868  cdleme0c  33869  cdleme0e  33873  cdleme0fN  33874  cdleme01N  33877  cdleme02N  33878  cdleme0ex1N  33879  cdleme0moN  33881  cdleme3g  33890  cdleme3h  33891  cdleme3  33893  cdleme4  33894  cdleme4a  33895  cdleme5  33896  cdleme8  33906  cdleme9  33909  cdleme10  33910  cdleme16aN  33915  cdleme11a  33916  cdleme11fN  33920  cdleme11g  33921  cdleme11h  33922  cdleme11j  33923  cdleme11k  33924  cdleme12  33927  cdleme13  33928  cdleme17c  33944  cdleme17d1  33945  cdleme18a  33947  cdleme18b  33948  cdleme18c  33949  cdleme22gb  33950  cdlemeda  33954  cdlemednpq  33955  cdlemednuN  33956  cdleme19c  33961  cdleme20aN  33965  cdleme20bN  33966  cdleme20c  33967  cdleme22aa  33995  cdleme22a  33996  cdleme22b  33997  cdleme22d  33999  cdleme22e  34000  cdleme27cl  34022  cdleme27a  34023  cdleme30a  34034  cdleme42a  34127  cdleme42c  34128  cdleme50laut  34203  cdlemf1  34217  cdlemf  34219  cdlemfnid  34220  trlord  34225  cdlemg2fv2  34256  cdlemg2kq  34258  cdlemg2m  34260  cdlemg4a  34264  cdlemg4d  34269  cdlemg4g  34272  cdlemg4  34273  cdlemg6c  34276  cdlemg7aN  34281  cdlemg8a  34283  cdlemg8b  34284  cdlemg8c  34285  cdlemg9a  34288  cdlemg9b  34289  cdlemg9  34290  cdlemg11aq  34294  cdlemg10c  34295  cdlemg12a  34299  cdlemg12b  34300  cdlemg12c  34301  cdlemg17a  34317  cdlemg18b  34335  cdlemg18c  34336  cdlemg31b0a  34351  cdlemg31a  34353  cdlemg31b  34354  cdlemg31d  34356  cdlemg35  34369  trlcoabs2N  34378  trlcolem  34382  cdlemg44a  34387  trljco  34396  trljco2  34397  tendoco2  34424  tendopltp  34436  cdlemi1  34474  cdlemi2  34475  cdlemj3  34479  tendocan  34480  cdlemk3  34489  cdlemk4  34490  cdlemk5a  34491  cdlemk9  34495  cdlemk9bN  34496  cdlemkvcl  34498  cdlemk10  34499  cdlemk30  34550  cdlemk31  34552  cdlemk39  34572  cdlemkfid1N  34577  cdlemkid1  34578  cdlemkid2  34580  cdlemkfid3N  34581  cdlemk19ylem  34586  cdlemk19xlem  34598  cdlemk19x  34599  cdlemk53b  34612  cdlemk53  34613  cdlemk54  34614  cdlemk55a  34615  cdlemk43N  34619  cdlemk19u1  34625  cdlemk19u  34626  cdleml1N  34632  erngdvlem4  34647  erngdvlem4-rN  34655  dia11N  34705  cdlemm10N  34775  dib11N  34817  cdlemn2  34852  cdlemn10  34863  dihjustlem  34873  dihord2cN  34878  dihlsscpre  34891  dih1dimb2  34898  dihvalcq2  34904  dihopelvalcpre  34905  dihord6b  34917  dih11  34922  dihmeetlem1N  34947  dihglblem2N  34951  dihglblem3N  34952  dihmeetlem2N  34956  dihglbcpreN  34957  dihmeetcN  34959  dihmeetbclemN  34961  dihmeetlem4preN  34963  dihmeetlem9N  34972  dihmeetlem20N  34983  dihlspsnssN  34989  dihlspsnat  34990  dihatlat  34991  dihglblem6  34997  dihmeet  35000  dochss  35022  hdmapval3N  35498  hgmap11  35562
  Copyright terms: Public domain W3C validator