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

Theorem simp1l 1021
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 1018 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  simpl1l  1048  simpr1l  1054  simp11l  1108  simp21l  1114  simp31l  1120  funprg  5627  tfisi  6678  omeulem2  7234  uniinqs  7393  unxpdomlem3  7728  elfiun  7892  cantnffval  8083  tcrank  8305  cofsmo  8652  isfin2-2  8702  tskint  9166  tskun  9167  tskurn  9170  gruina  9199  dedekind  9747  dmdcan  10261  lt2msq1  10435  supmullem1  10516  supmul  10518  xaddass  11452  xaddass2  11453  xlt2add  11463  xmulasslem3  11489  xadddi2r  11501  iccsplit  11664  expaddzlem  12191  expaddz  12192  expmulz  12194  ccatopth2  12678  swrdccat3  12699  resqrtcl  13069  limsupgle  13282  o1add  13418  o1mul  13419  o1sub  13420  bitsfzo  14067  sadfval  14084  smufval  14109  prmexpb  14240  4sqlem18  14462  vdwlem10  14490  fsets  14640  submre  14984  mrelatlub  15795  mndodcong  16545  subgabl  16823  gex2abl  16836  cntzsubr  17440  abvres  17467  lbsind2  17706  lspsneu  17748  lbsextlem2  17784  lbsextg  17787  lindfind2  18831  matring  18923  maducoeval  19119  maducoeval2  19120  maduf  19121  madurid  19124  gsummatr01  19139  cramerimplem3  19165  cnprest  19768  hausnei2  19832  isreg2  19856  cmpcld  19880  llyrest  19964  nllyrest  19965  csdfil  20373  hausflimlem  20458  ssblps  20903  ssbl  20904  dvres2  22294  plyadd  22592  plymul  22593  coeeu  22600  vieta1  22686  aalioulem3  22708  aalioulem4  22709  efgh  22906  cxpadd  23038  cxpsub  23041  mulcxp  23044  divcxp  23046  cxple2  23056  cxplt2  23057  cxpcn3lem  23099  angcan  23112  ang180lem5  23123  isosctrlem3  23132  logexprlim  23478  abvcxp  23778  padicabv  23793  brbtwn2  24186  ax5seglem6  24215  axcontlem4  24248  axcontlem8  24252  clwwlknimp  24754  chscllem4  26536  ogrpinvlt  27692  poseq  29309  wsuclem  29357  nofulllem5  29442  ifscgr  29670  congtr  30879  fzmaxdif  30895  isnumbasgrplem2  31029  mullimc  31576  mullimcf  31583  islpcn  31599  cncfuni  31643  icccncfext  31644  stoweidlem34  31770  stoweidlem59  31795  stirlinglem13  31822  fourierdlem41  31884  fourierdlem42  31885  fourierdlem73  31916  lincscm  32901  lincext3  32927  el0ldep  32937  el0ldepsnzr  32938  lshpnelb  34584  lfl1  34670  lshpkrlem6  34715  lshpkrex  34718  hlrelat3  35011  atbtwnexOLDN  35046  atbtwnex  35047  3dim3  35068  3atlem5  35086  2llnmat  35123  lvolex3N  35137  lvolnle3at  35181  4atlem11  35208  4atlem12  35211  dalemccea  35282  cdlema2N  35391  paddasslem2  35420  atmod1i1m  35457  lhp2lt  35600  lhp0lt  35602  lhpj1  35621  lhpmcvr4N  35625  lhpelim  35636  lhpmod2i2  35637  lhpmod6i1  35638  cdlemb2  35640  lhple  35641  lhpat  35642  4atex  35675  4atex2-0aOLDN  35677  4atex3  35680  ldilco  35715  ltrncl  35724  ltrn11  35725  ltrnle  35728  ltrncnvleN  35729  ltrnm  35730  ltrnj  35731  ltrncvr  35732  ltrnatb  35736  ltrnel  35738  ltrncnvel  35741  ltrncnv  35745  ltrnmwOLD  35751  trlval2  35763  trlcnv  35765  trljat1  35766  trljat2  35767  trl0  35770  ltrnnidn  35774  trlnidatb  35777  cdlemc1  35791  cdlemc2  35792  cdlemc5  35795  cdlemc6  35796  cdlemd3  35800  cdlemd6  35803  cdleme0aa  35810  cdleme0b  35812  cdleme0c  35813  cdleme0e  35817  cdleme0fN  35818  cdleme01N  35821  cdleme02N  35822  cdleme0ex1N  35823  cdleme0moN  35825  cdleme3g  35834  cdleme3h  35835  cdleme3  35837  cdleme4  35838  cdleme4a  35839  cdleme5  35840  cdleme8  35850  cdleme9  35853  cdleme10  35854  cdleme16aN  35859  cdleme11a  35860  cdleme11fN  35864  cdleme11g  35865  cdleme11h  35866  cdleme11j  35867  cdleme11k  35868  cdleme12  35871  cdleme13  35872  cdleme17c  35888  cdleme17d1  35889  cdleme18a  35891  cdleme18b  35892  cdleme18c  35893  cdleme22gb  35894  cdlemeda  35898  cdlemednpq  35899  cdlemednuN  35900  cdleme19c  35906  cdleme20aN  35910  cdleme20bN  35911  cdleme20c  35912  cdleme22aa  35940  cdleme22a  35941  cdleme22b  35942  cdleme22d  35944  cdleme22e  35945  cdleme27cl  35967  cdleme27a  35968  cdleme30a  35979  cdleme42a  36072  cdleme42c  36073  cdleme50laut  36148  cdlemf1  36162  cdlemf  36164  cdlemfnid  36165  trlord  36170  cdlemg2fv2  36201  cdlemg2kq  36203  cdlemg2m  36205  cdlemg4a  36209  cdlemg4d  36214  cdlemg4g  36217  cdlemg4  36218  cdlemg6c  36221  cdlemg7aN  36226  cdlemg8a  36228  cdlemg8b  36229  cdlemg8c  36230  cdlemg9a  36233  cdlemg9b  36234  cdlemg9  36235  cdlemg11aq  36239  cdlemg10c  36240  cdlemg12a  36244  cdlemg12b  36245  cdlemg12c  36246  cdlemg17a  36262  cdlemg18b  36280  cdlemg18c  36281  cdlemg31b0a  36296  cdlemg31a  36298  cdlemg31b  36299  cdlemg31d  36301  cdlemg35  36314  trlcoabs2N  36323  trlcolem  36327  cdlemg44a  36332  trljco  36341  trljco2  36342  tendoco2  36369  tendopltp  36381  cdlemi1  36419  cdlemi2  36420  cdlemj3  36424  tendocan  36425  cdlemk3  36434  cdlemk4  36435  cdlemk5a  36436  cdlemk9  36440  cdlemk9bN  36441  cdlemkvcl  36443  cdlemk10  36444  cdlemk30  36495  cdlemk31  36497  cdlemk39  36517  cdlemkfid1N  36522  cdlemkid1  36523  cdlemkid2  36525  cdlemkfid3N  36526  cdlemk19ylem  36531  cdlemk19xlem  36543  cdlemk19x  36544  cdlemk53b  36557  cdlemk53  36558  cdlemk54  36559  cdlemk55a  36560  cdlemk43N  36564  cdlemk19u1  36570  cdlemk19u  36571  cdleml1N  36577  erngdvlem4  36592  erngdvlem4-rN  36600  dia11N  36650  cdlemm10N  36720  dib11N  36762  cdlemn2  36797  cdlemn10  36808  dihjustlem  36818  dihord2cN  36823  dihlsscpre  36836  dih1dimb2  36843  dihvalcq2  36849  dihopelvalcpre  36850  dihord6b  36862  dih11  36867  dihmeetlem1N  36892  dihglblem2N  36896  dihglblem3N  36897  dihmeetlem2N  36901  dihglbcpreN  36902  dihmeetcN  36904  dihmeetbclemN  36906  dihmeetlem4preN  36908  dihmeetlem9N  36917  dihmeetlem20N  36928  dihlspsnssN  36934  dihlspsnat  36935  dihatlat  36936  dihglblem6  36942  dihmeet  36945  dochss  36967  hdmapval3N  37443  hgmap11  37507
  Copyright terms: Public domain W3C validator