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

Theorem simp1l 1018
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 455 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 1015 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simpl1l  1045  simpr1l  1051  simp11l  1105  simp21l  1111  simp31l  1117  funprg  5558  tfisi  6610  omeulem2  7168  uniinqs  7327  unxpdomlem3  7660  elfiun  7823  cantnffval  8011  tcrank  8233  cofsmo  8580  isfin2-2  8630  tskint  9092  tskun  9093  tskurn  9096  gruina  9125  dedekind  9673  dmdcan  10189  lt2msq1  10362  supmullem1  10443  supmul  10445  xaddass  11380  xaddass2  11381  xlt2add  11391  xmulasslem3  11417  xadddi2r  11429  iccsplit  11592  expaddzlem  12131  expaddz  12132  expmulz  12134  ccatopth2  12626  swrdccat3  12647  resqrtcl  13108  limsupgle  13321  o1add  13457  o1mul  13458  o1sub  13459  bitsfzo  14106  sadfval  14123  smufval  14148  prmexpb  14279  4sqlem18  14501  vdwlem10  14529  fsets  14681  submre  15031  mrelatlub  15952  mndodcong  16702  subgabl  16980  gex2abl  16993  cntzsubr  17593  abvres  17620  lbsind2  17859  lspsneu  17901  lbsextlem2  17937  lbsextg  17940  lindfind2  18957  matring  19049  maducoeval  19245  maducoeval2  19246  maduf  19247  madurid  19250  gsummatr01  19265  cramerimplem3  19291  cnprest  19895  hausnei2  19959  isreg2  19983  cmpcld  20007  llyrest  20090  nllyrest  20091  csdfil  20499  hausflimlem  20584  ssblps  21029  ssbl  21030  dvres2  22420  plyadd  22718  plymul  22719  coeeu  22726  vieta1  22812  aalioulem3  22834  aalioulem4  22835  efgh  23032  cxpadd  23166  cxpsub  23169  mulcxp  23172  divcxp  23174  cxple2  23184  cxplt2  23185  cxpcn3lem  23227  angcan  23271  ang180lem5  23282  isosctrlem3  23289  logexprlim  23636  abvcxp  23936  padicabv  23951  brbtwn2  24350  ax5seglem6  24379  axcontlem4  24412  axcontlem8  24416  clwwlknimp  24918  chscllem4  26696  ogrpinvlt  27897  poseq  29534  wsuclem  29582  nofulllem5  29667  ifscgr  29883  congtr  31104  fzmaxdif  31120  isnumbasgrplem2  31257  mullimc  31823  mullimcf  31830  islpcn  31846  cncfuni  31890  icccncfext  31891  stoweidlem34  32017  stoweidlem59  32042  stirlinglem13  32069  fourierdlem41  32131  fourierdlem42  32132  fourierdlem73  32163  pfxccat3  32636  lincscm  33266  lincext3  33292  el0ldep  33302  el0ldepsnzr  33303  lshpnelb  35157  lfl1  35243  lshpkrlem6  35288  lshpkrex  35291  hlrelat3  35584  atbtwnexOLDN  35619  atbtwnex  35620  3dim3  35641  3atlem5  35659  2llnmat  35696  lvolex3N  35710  lvolnle3at  35754  4atlem11  35781  4atlem12  35784  dalemccea  35855  cdlema2N  35964  paddasslem2  35993  atmod1i1m  36030  lhp2lt  36173  lhp0lt  36175  lhpj1  36194  lhpmcvr4N  36198  lhpelim  36209  lhpmod2i2  36210  lhpmod6i1  36211  cdlemb2  36213  lhple  36214  lhpat  36215  4atex  36248  4atex2-0aOLDN  36250  4atex3  36253  ldilco  36288  ltrncl  36297  ltrn11  36298  ltrnle  36301  ltrncnvleN  36302  ltrnm  36303  ltrnj  36304  ltrncvr  36305  ltrnatb  36309  ltrnel  36311  ltrncnvel  36314  ltrncnv  36318  ltrnmwOLD  36324  trlval2  36336  trlcnv  36338  trljat1  36339  trljat2  36340  trl0  36343  ltrnnidn  36347  trlnidatb  36350  cdlemc1  36364  cdlemc2  36365  cdlemc5  36368  cdlemc6  36369  cdlemd3  36373  cdlemd6  36376  cdleme0aa  36383  cdleme0b  36385  cdleme0c  36386  cdleme0e  36390  cdleme0fN  36391  cdleme01N  36394  cdleme02N  36395  cdleme0ex1N  36396  cdleme0moN  36398  cdleme3g  36407  cdleme3h  36408  cdleme3  36410  cdleme4  36411  cdleme4a  36412  cdleme5  36413  cdleme8  36423  cdleme9  36426  cdleme10  36427  cdleme16aN  36432  cdleme11a  36433  cdleme11fN  36437  cdleme11g  36438  cdleme11h  36439  cdleme11j  36440  cdleme11k  36441  cdleme12  36444  cdleme13  36445  cdleme17c  36461  cdleme17d1  36462  cdleme18a  36464  cdleme18b  36465  cdleme18c  36466  cdleme22gb  36467  cdlemeda  36471  cdlemednpq  36472  cdlemednuN  36473  cdleme19c  36479  cdleme20aN  36483  cdleme20bN  36484  cdleme20c  36485  cdleme22aa  36513  cdleme22a  36514  cdleme22b  36515  cdleme22d  36517  cdleme22e  36518  cdleme27cl  36540  cdleme27a  36541  cdleme30a  36552  cdleme42a  36645  cdleme42c  36646  cdleme50laut  36721  cdlemf1  36735  cdlemf  36737  cdlemfnid  36738  trlord  36743  cdlemg2fv2  36774  cdlemg2kq  36776  cdlemg2m  36778  cdlemg4a  36782  cdlemg4d  36787  cdlemg4g  36790  cdlemg4  36791  cdlemg6c  36794  cdlemg7aN  36799  cdlemg8a  36801  cdlemg8b  36802  cdlemg8c  36803  cdlemg9a  36806  cdlemg9b  36807  cdlemg9  36808  cdlemg11aq  36812  cdlemg10c  36813  cdlemg12a  36817  cdlemg12b  36818  cdlemg12c  36819  cdlemg17a  36835  cdlemg18b  36853  cdlemg18c  36854  cdlemg31b0a  36869  cdlemg31a  36871  cdlemg31b  36872  cdlemg31d  36874  cdlemg35  36887  trlcoabs2N  36896  trlcolem  36900  cdlemg44a  36905  trljco  36914  trljco2  36915  tendoco2  36942  tendopltp  36954  cdlemi1  36992  cdlemi2  36993  cdlemj3  36997  tendocan  36998  cdlemk3  37007  cdlemk4  37008  cdlemk5a  37009  cdlemk9  37013  cdlemk9bN  37014  cdlemkvcl  37016  cdlemk10  37017  cdlemk30  37068  cdlemk31  37070  cdlemk39  37090  cdlemkfid1N  37095  cdlemkid1  37096  cdlemkid2  37098  cdlemkfid3N  37099  cdlemk19ylem  37104  cdlemk19xlem  37116  cdlemk19x  37117  cdlemk53b  37130  cdlemk53  37131  cdlemk54  37132  cdlemk55a  37133  cdlemk43N  37137  cdlemk19u1  37143  cdlemk19u  37144  cdleml1N  37150  erngdvlem4  37165  erngdvlem4-rN  37173  dia11N  37223  cdlemm10N  37293  dib11N  37335  cdlemn2  37370  cdlemn10  37381  dihjustlem  37391  dihord2cN  37396  dihlsscpre  37409  dih1dimb2  37416  dihvalcq2  37422  dihopelvalcpre  37423  dihord6b  37435  dih11  37440  dihmeetlem1N  37465  dihglblem2N  37469  dihglblem3N  37470  dihmeetlem2N  37474  dihglbcpreN  37475  dihmeetcN  37477  dihmeetbclemN  37479  dihmeetlem4preN  37481  dihmeetlem9N  37490  dihmeetlem20N  37501  dihlspsnssN  37507  dihlspsnat  37508  dihatlat  37509  dihglblem6  37515  dihmeet  37518  dochss  37540  hdmapval3N  38016  hgmap11  38080
  Copyright terms: Public domain W3C validator