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

Theorem simp1l 1031
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 459 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 1028 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 984
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 189  df-an 373  df-3an 986
This theorem is referenced by:  simpl1l  1058  simpr1l  1064  simp11l  1118  simp21l  1124  simp31l  1130  funprg  5630  tfisi  6682  omeulem2  7281  uniinqs  7440  unxpdomlem3  7775  elfiun  7941  cantnffval  8165  tcrank  8352  cofsmo  8696  isfin2-2  8746  tskint  9207  tskun  9208  tskurn  9211  gruina  9240  dedekind  9794  dmdcan  10314  lt2msq1  10487  supmullem1  10574  supmul  10576  xaddass  11532  xaddass2  11533  xlt2add  11543  xmulasslem3  11569  xadddi2r  11581  iccsplit  11762  expaddzlem  12312  expaddz  12313  expmulz  12315  ccatopth2  12822  swrdccat3  12843  resqrtcl  13310  limsupgle  13528  o1add  13670  o1mul  13671  o1sub  13672  bitsfzo  14402  sadfval  14419  smufval  14444  prmexpb  14663  4sqlem18OLD  14899  4sqlem18  14905  vdwlem10  14933  fsets  15142  submre  15504  mrelatlub  16425  mndodcong  17184  subgabl  17469  gex2abl  17482  cntzsubr  18033  abvres  18060  lbsind2  18297  lspsneu  18339  lbsextlem2  18375  lbsextg  18378  lindfind2  19369  matring  19461  maducoeval  19657  maducoeval2  19658  maduf  19659  madurid  19662  gsummatr01  19677  cramerimplem3  19703  cnprest  20298  hausnei2  20362  isreg2  20386  cmpcld  20410  llyrest  20493  nllyrest  20494  csdfil  20902  hausflimlem  20987  ssblps  21430  ssbl  21431  dvres2  22860  plyadd  23164  plymul  23165  coeeu  23172  vieta1  23258  aalioulem3  23283  aalioulem4  23284  efgh  23483  cxpadd  23617  cxpsub  23620  mulcxp  23623  divcxp  23625  cxple2  23635  cxplt2  23636  cxpcn3lem  23680  angcan  23724  ang180lem5  23735  isosctrlem3  23742  logexprlim  24146  abvcxp  24446  padicabv  24461  brbtwn2  24928  ax5seglem6  24957  axcontlem4  24990  axcontlem8  24994  clwwlknimp  25497  chscllem4  27286  ogrpinvlt  28480  poseq  30484  wsuclem  30501  nofulllem5  30588  ifscgr  30804  lshpnelb  32544  lfl1  32630  lshpkrlem6  32675  lshpkrex  32678  hlrelat3  32971  atbtwnexOLDN  33006  atbtwnex  33007  3dim3  33028  3atlem5  33046  2llnmat  33083  lvolex3N  33097  lvolnle3at  33141  4atlem11  33168  4atlem12  33171  dalemccea  33242  cdlema2N  33351  paddasslem2  33380  atmod1i1m  33417  lhp2lt  33560  lhp0lt  33562  lhpj1  33581  lhpmcvr4N  33585  lhpelim  33596  lhpmod2i2  33597  lhpmod6i1  33598  cdlemb2  33600  lhple  33601  lhpat  33602  4atex  33635  4atex2-0aOLDN  33637  4atex3  33640  ldilco  33675  ltrncl  33684  ltrn11  33685  ltrnle  33688  ltrncnvleN  33689  ltrnm  33690  ltrnj  33691  ltrncvr  33692  ltrnatb  33696  ltrnel  33698  ltrncnvel  33701  ltrncnv  33705  ltrnmwOLD  33711  trlval2  33723  trlcnv  33725  trljat1  33726  trljat2  33727  trl0  33730  ltrnnidn  33734  trlnidatb  33737  cdlemc1  33751  cdlemc2  33752  cdlemc5  33755  cdlemc6  33756  cdlemd3  33760  cdlemd6  33763  cdleme0aa  33770  cdleme0b  33772  cdleme0c  33773  cdleme0e  33777  cdleme0fN  33778  cdleme01N  33781  cdleme02N  33782  cdleme0ex1N  33783  cdleme0moN  33785  cdleme3g  33794  cdleme3h  33795  cdleme3  33797  cdleme4  33798  cdleme4a  33799  cdleme5  33800  cdleme8  33810  cdleme9  33813  cdleme10  33814  cdleme16aN  33819  cdleme11a  33820  cdleme11fN  33824  cdleme11g  33825  cdleme11h  33826  cdleme11j  33827  cdleme11k  33828  cdleme12  33831  cdleme13  33832  cdleme17c  33848  cdleme17d1  33849  cdleme18a  33851  cdleme18b  33852  cdleme18c  33853  cdleme22gb  33854  cdlemeda  33858  cdlemednpq  33859  cdlemednuN  33860  cdleme19c  33866  cdleme20aN  33870  cdleme20bN  33871  cdleme20c  33872  cdleme22aa  33900  cdleme22a  33901  cdleme22b  33902  cdleme22d  33904  cdleme22e  33905  cdleme27cl  33927  cdleme27a  33928  cdleme30a  33939  cdleme42a  34032  cdleme42c  34033  cdleme50laut  34108  cdlemf1  34122  cdlemf  34124  cdlemfnid  34125  trlord  34130  cdlemg2fv2  34161  cdlemg2kq  34163  cdlemg2m  34165  cdlemg4a  34169  cdlemg4d  34174  cdlemg4g  34177  cdlemg4  34178  cdlemg6c  34181  cdlemg7aN  34186  cdlemg8a  34188  cdlemg8b  34189  cdlemg8c  34190  cdlemg9a  34193  cdlemg9b  34194  cdlemg9  34195  cdlemg11aq  34199  cdlemg10c  34200  cdlemg12a  34204  cdlemg12b  34205  cdlemg12c  34206  cdlemg17a  34222  cdlemg18b  34240  cdlemg18c  34241  cdlemg31b0a  34256  cdlemg31a  34258  cdlemg31b  34259  cdlemg31d  34261  cdlemg35  34274  trlcoabs2N  34283  trlcolem  34287  cdlemg44a  34292  trljco  34301  trljco2  34302  tendoco2  34329  tendopltp  34341  cdlemi1  34379  cdlemi2  34380  cdlemj3  34384  tendocan  34385  cdlemk3  34394  cdlemk4  34395  cdlemk5a  34396  cdlemk9  34400  cdlemk9bN  34401  cdlemkvcl  34403  cdlemk10  34404  cdlemk30  34455  cdlemk31  34457  cdlemk39  34477  cdlemkfid1N  34482  cdlemkid1  34483  cdlemkid2  34485  cdlemkfid3N  34486  cdlemk19ylem  34491  cdlemk19xlem  34503  cdlemk19x  34504  cdlemk53b  34517  cdlemk53  34518  cdlemk54  34519  cdlemk55a  34520  cdlemk43N  34524  cdlemk19u1  34530  cdlemk19u  34531  cdleml1N  34537  erngdvlem4  34552  erngdvlem4-rN  34560  dia11N  34610  cdlemm10N  34680  dib11N  34722  cdlemn2  34757  cdlemn10  34768  dihjustlem  34778  dihord2cN  34783  dihlsscpre  34796  dih1dimb2  34803  dihvalcq2  34809  dihopelvalcpre  34810  dihord6b  34822  dih11  34827  dihmeetlem1N  34852  dihglblem2N  34856  dihglblem3N  34857  dihmeetlem2N  34861  dihglbcpreN  34862  dihmeetcN  34864  dihmeetbclemN  34866  dihmeetlem4preN  34868  dihmeetlem9N  34877  dihmeetlem20N  34888  dihlspsnssN  34894  dihlspsnat  34895  dihatlat  34896  dihglblem6  34902  dihmeet  34905  dochss  34927  hdmapval3N  35403  hgmap11  35467  congtr  35809  fzmaxdif  35825  isnumbasgrplem2  35957  mullimc  37690  mullimcf  37697  islpcn  37713  cncfuni  37758  icccncfext  37759  stoweidlem34  37889  stoweidlem59  37914  stirlinglem13  37942  fourierdlem41  38005  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem73  38037  sge0iunmptlemfi  38249  meadjiunlem  38297  ovncvrrp  38380  pfxccat3  38961  nbgrisvtx  39410  nbupgrres  39421  lincscm  40210  lincext3  40236  el0ldep  40246  el0ldepsnzr  40247
  Copyright terms: Public domain W3C validator