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

Theorem simp1l 1020
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 1017 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  simpl1l  1047  simpr1l  1053  simp11l  1107  simp21l  1113  simp31l  1119  funprg  5635  tfisi  6671  omeulem2  7229  uniinqs  7388  unxpdomlem3  7723  elfiun  7886  cantnffval  8076  tcrank  8298  cofsmo  8645  isfin2-2  8695  tskint  9159  tskun  9160  tskurn  9163  gruina  9192  dedekind  9739  dmdcan  10250  lt2msq1  10424  supmullem1  10505  supmul  10507  xaddass  11437  xaddass2  11438  xlt2add  11448  xmulasslem3  11474  xadddi2r  11486  iccsplit  11649  expaddzlem  12171  expaddz  12172  expmulz  12174  ccatopth2  12653  swrdccat3  12674  resqrtcl  13044  limsupgle  13256  o1add  13392  o1mul  13393  o1sub  13394  bitsfzo  13937  sadfval  13954  smufval  13979  prmexpb  14110  4sqlem18  14332  vdwlem10  14360  fsets  14509  submre  14853  mrelatlub  15666  mndodcong  16359  subgabl  16634  gex2abl  16647  cntzsubr  17241  abvres  17268  lbsind2  17507  lspsneu  17549  lbsextlem2  17585  lbsextg  17588  lindfind2  18617  matrng  18709  maducoeval  18905  maducoeval2  18906  maduf  18907  madurid  18910  gsummatr01  18925  cramerimplem3  18951  cnprest  19553  hausnei2  19617  isreg2  19641  cmpcld  19665  llyrest  19749  nllyrest  19750  csdfil  20127  hausflimlem  20212  ssblps  20657  ssbl  20658  dvres2  22048  plyadd  22346  plymul  22347  coeeu  22354  vieta1  22439  aalioulem3  22461  aalioulem4  22462  cxpadd  22785  cxpsub  22788  mulcxp  22791  divcxp  22793  cxple2  22803  cxplt2  22804  cxpcn3lem  22846  angcan  22859  ang180lem5  22870  isosctrlem3  22879  logexprlim  23225  abvcxp  23525  padicabv  23540  brbtwn2  23881  ax5seglem6  23910  axcontlem4  23943  axcontlem8  23947  clwwlknimp  24449  chscllem4  26231  ogrpinvlt  27373  poseq  28907  wsuclem  28955  nofulllem5  29040  ifscgr  29268  congtr  30505  fzmaxdif  30521  isnumbasgrplem2  30657  mullimc  31158  mullimcf  31165  islpcn  31181  cncfuni  31225  icccncfext  31226  stoweidlem34  31334  stoweidlem59  31359  stirlinglem13  31386  fourierdlem41  31448  fourierdlem42  31449  fourierdlem73  31480  lincscm  32104  lincext3  32130  el0ldep  32140  el0ldepsnzr  32141  lshpnelb  33781  lfl1  33867  lshpkrlem6  33912  lshpkrex  33915  hlrelat3  34208  atbtwnexOLDN  34243  atbtwnex  34244  3dim3  34265  3atlem5  34283  2llnmat  34320  lvolex3N  34334  lvolnle3at  34378  4atlem11  34405  4atlem12  34408  dalemccea  34479  cdlema2N  34588  paddasslem2  34617  atmod1i1m  34654  lhp2lt  34797  lhp0lt  34799  lhpj1  34818  lhpmcvr4N  34822  lhpelim  34833  lhpmod2i2  34834  lhpmod6i1  34835  cdlemb2  34837  lhple  34838  lhpat  34839  4atex  34872  4atex2-0aOLDN  34874  4atex3  34877  ldilco  34912  ltrncl  34921  ltrn11  34922  ltrnle  34925  ltrncnvleN  34926  ltrnm  34927  ltrnj  34928  ltrncvr  34929  ltrnatb  34933  ltrnel  34935  ltrncnvel  34938  ltrncnv  34942  ltrnmw  34947  trlval2  34959  trlcnv  34961  trljat1  34962  trljat2  34963  trl0  34966  ltrnnidn  34970  trlnidatb  34973  cdlemc1  34987  cdlemc2  34988  cdlemc5  34991  cdlemc6  34992  cdlemd3  34996  cdlemd6  34999  cdleme0aa  35006  cdleme0b  35008  cdleme0c  35009  cdleme0e  35013  cdleme0fN  35014  cdleme01N  35017  cdleme02N  35018  cdleme0ex1N  35019  cdleme0moN  35021  cdleme3g  35030  cdleme3h  35031  cdleme3  35033  cdleme4  35034  cdleme4a  35035  cdleme5  35036  cdleme8  35046  cdleme9  35049  cdleme10  35050  cdleme16aN  35055  cdleme11a  35056  cdleme11fN  35060  cdleme11g  35061  cdleme11h  35062  cdleme11j  35063  cdleme11k  35064  cdleme12  35067  cdleme13  35068  cdleme17c  35084  cdleme17d1  35085  cdleme18a  35087  cdleme18b  35088  cdleme18c  35089  cdleme22gb  35090  cdlemeda  35094  cdlemednpq  35095  cdlemednuN  35096  cdleme19c  35101  cdleme20aN  35105  cdleme20bN  35106  cdleme20c  35107  cdleme22aa  35135  cdleme22a  35136  cdleme22b  35137  cdleme22d  35139  cdleme22e  35140  cdleme27cl  35162  cdleme27a  35163  cdleme30a  35174  cdleme42a  35267  cdleme42c  35268  cdleme50laut  35343  cdlemf1  35357  cdlemf  35359  cdlemfnid  35360  trlord  35365  cdlemg2fv2  35396  cdlemg2kq  35398  cdlemg2m  35400  cdlemg4a  35404  cdlemg4d  35409  cdlemg4g  35412  cdlemg4  35413  cdlemg6c  35416  cdlemg7aN  35421  cdlemg8a  35423  cdlemg8b  35424  cdlemg8c  35425  cdlemg9a  35428  cdlemg9b  35429  cdlemg9  35430  cdlemg11aq  35434  cdlemg10c  35435  cdlemg12a  35439  cdlemg12b  35440  cdlemg12c  35441  cdlemg17a  35457  cdlemg18b  35475  cdlemg18c  35476  cdlemg31b0a  35491  cdlemg31a  35493  cdlemg31b  35494  cdlemg31d  35496  cdlemg35  35509  trlcoabs2N  35518  trlcolem  35522  cdlemg44a  35527  trljco  35536  trljco2  35537  tendoco2  35564  tendopltp  35576  cdlemi1  35614  cdlemi2  35615  cdlemj3  35619  tendocan  35620  cdlemk3  35629  cdlemk4  35630  cdlemk5a  35631  cdlemk9  35635  cdlemk9bN  35636  cdlemkvcl  35638  cdlemk10  35639  cdlemk30  35690  cdlemk31  35692  cdlemk39  35712  cdlemkfid1N  35717  cdlemkid1  35718  cdlemkid2  35720  cdlemkfid3N  35721  cdlemk19ylem  35726  cdlemk19xlem  35738  cdlemk19x  35739  cdlemk53b  35752  cdlemk53  35753  cdlemk54  35754  cdlemk55a  35755  cdlemk43N  35759  cdlemk19u1  35765  cdlemk19u  35766  cdleml1N  35772  erngdvlem4  35787  erngdvlem4-rN  35795  dia11N  35845  cdlemm10N  35915  dib11N  35957  cdlemn2  35992  cdlemn10  36003  dihjustlem  36013  dihord2cN  36018  dihlsscpre  36031  dih1dimb2  36038  dihvalcq2  36044  dihopelvalcpre  36045  dihord6b  36057  dih11  36062  dihmeetlem1N  36087  dihglblem2N  36091  dihglblem3N  36092  dihmeetlem2N  36096  dihglbcpreN  36097  dihmeetcN  36099  dihmeetbclemN  36101  dihmeetlem4preN  36103  dihmeetlem9N  36112  dihmeetlem20N  36123  dihlspsnssN  36129  dihlspsnat  36130  dihatlat  36131  dihglblem6  36137  dihmeet  36140  dochss  36162  hdmapval3N  36638  hgmap11  36702
  Copyright terms: Public domain W3C validator