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

Theorem simp1l 979
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 443 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl1l  1006  simpr1l  1012  simp11l  1066  simp21l  1072  simp31l  1078  tfisi  4651  funprg  5303  omeulem2  6583  unxpdomlem3  7071  elfiun  7185  cantnffval  7366  tcrank  7556  cofsmo  7897  isfin2-2  7947  tskint  8409  tskun  8410  tskurn  8413  gruina  8442  dmdcan  9472  lt2msq1  9641  supmullem1  9722  supmul  9724  xaddass  10571  xaddass2  10572  xlt2add  10582  xmulasslem3  10608  xadddi2r  10620  iccsplit  10770  expaddzlem  11147  expaddz  11148  expmulz  11150  ccatopth2  11465  resqrcl  11741  limsupgle  11953  o1add  12089  o1mul  12090  o1sub  12091  bitsfzo  12628  sadfval  12645  smufval  12670  prmexpb  12798  4sqlem18  13011  vdwlem10  13039  submre  13509  mrelatlub  14291  spwpr4  14342  mndodcong  14859  subgabl  15134  gex2abl  15145  cntzsubr  15579  abvres  15606  lbsind2  15836  lspsneu  15878  lbsextlem2  15914  lbsextg  15917  cnprest  17019  hausnei2  17083  isreg2  17107  cmpcld  17131  llyrest  17213  nllyrest  17214  csdfil  17591  hausflimlem  17676  ssbl  17973  dvres2  19264  plyadd  19601  plymul  19602  coeeu  19609  vieta1  19694  aalioulem3  19716  aalioulem4  19717  cxpadd  20028  cxpsub  20031  mulcxp  20034  divcxp  20036  cxple2  20046  cxplt2  20047  cxpcn3lem  20089  angcan  20102  ang180lem5  20113  isosctrlem3  20122  logexprlim  20466  abvcxp  20766  padicabv  20781  chscllem4  22221  dedekind  24084  poseq  24255  nofulllem5  24362  brbtwn2  24535  ax5seglem6  24564  axcontlem4  24597  axcontlem8  24601  ifscgr  24669  uninqs  25050  intopcoaconlem3b  25549  prdnei  25584  islimrs  25591  flfneic  25635  setiscat  25990  congtr  27063  fzmaxdif  27079  isnumbasgrplem2  27280  lindfind2  27299  matrng  27491  refsumcn  27712  fmuldfeq  27724  stoweidlem31  27791  stoweidlem34  27794  stoweidlem43  27803  stoweidlem46  27806  stoweidlem52  27812  stoweidlem53  27813  stoweidlem54  27814  stoweidlem55  27815  stoweidlem56  27816  stoweidlem57  27817  stoweidlem58  27818  stoweidlem59  27819  stoweidlem60  27820  stoweid  27823  stirlinglem13  27846  lshpnelb  29247  lfl1  29333  lshpkrlem6  29378  lshpkrex  29381  hlrelat3  29674  atbtwnexOLDN  29709  atbtwnex  29710  3dim3  29731  3atlem5  29749  2llnmat  29786  lvolex3N  29800  lvolnle3at  29844  4atlem11  29871  4atlem12  29874  dalemccea  29945  cdlema2N  30054  paddasslem2  30083  atmod1i1m  30120  lhp2lt  30263  lhp0lt  30265  lhpj1  30284  lhpmcvr4N  30288  lhpelim  30299  lhpmod2i2  30300  lhpmod6i1  30301  cdlemb2  30303  lhple  30304  lhpat  30305  4atex  30338  4atex2-0aOLDN  30340  4atex3  30343  ldilco  30378  ltrncl  30387  ltrn11  30388  ltrnle  30391  ltrncnvleN  30392  ltrnm  30393  ltrnj  30394  ltrncvr  30395  ltrnatb  30399  ltrnel  30401  ltrncnvel  30404  ltrncnv  30408  ltrnmw  30413  trlval2  30425  trlcnv  30427  trljat1  30428  trljat2  30429  trl0  30432  ltrnnidn  30436  trlnidatb  30439  cdlemc1  30453  cdlemc2  30454  cdlemc5  30457  cdlemc6  30458  cdlemd3  30462  cdlemd6  30465  cdleme0aa  30472  cdleme0b  30474  cdleme0c  30475  cdleme0e  30479  cdleme0fN  30480  cdleme01N  30483  cdleme02N  30484  cdleme0ex1N  30485  cdleme0moN  30487  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme4  30500  cdleme4a  30501  cdleme5  30502  cdleme8  30512  cdleme9  30515  cdleme10  30516  cdleme16aN  30521  cdleme11a  30522  cdleme11fN  30526  cdleme11g  30527  cdleme11h  30528  cdleme11j  30529  cdleme11k  30530  cdleme12  30533  cdleme13  30534  cdleme17c  30550  cdleme17d1  30551  cdleme18a  30553  cdleme18b  30554  cdleme18c  30555  cdleme22gb  30556  cdlemeda  30560  cdlemednpq  30561  cdlemednuN  30562  cdleme19c  30567  cdleme20aN  30571  cdleme20bN  30572  cdleme20c  30573  cdleme22aa  30601  cdleme22a  30602  cdleme22b  30603  cdleme22d  30605  cdleme22e  30606  cdleme27cl  30628  cdleme27a  30629  cdleme30a  30640  cdleme42a  30733  cdleme42c  30734  cdleme50laut  30809  cdlemf1  30823  cdlemf  30825  cdlemfnid  30826  trlord  30831  cdlemg2fv2  30862  cdlemg2kq  30864  cdlemg2m  30866  cdlemg4a  30870  cdlemg4d  30875  cdlemg4g  30878  cdlemg4  30879  cdlemg6c  30882  cdlemg7aN  30887  cdlemg8a  30889  cdlemg8b  30890  cdlemg8c  30891  cdlemg9a  30894  cdlemg9b  30895  cdlemg9  30896  cdlemg11aq  30900  cdlemg10c  30901  cdlemg12a  30905  cdlemg12b  30906  cdlemg12c  30907  cdlemg17a  30923  cdlemg18b  30941  cdlemg18c  30942  cdlemg31b0a  30957  cdlemg31a  30959  cdlemg31b  30960  cdlemg31d  30962  cdlemg35  30975  trlcoabs2N  30984  trlcolem  30988  cdlemg44a  30993  trljco  31002  trljco2  31003  tendoco2  31030  tendopltp  31042  cdlemi1  31080  cdlemi2  31081  cdlemj3  31085  tendocan  31086  cdlemk3  31095  cdlemk4  31096  cdlemk5a  31097  cdlemk9  31101  cdlemk9bN  31102  cdlemkvcl  31104  cdlemk10  31105  cdlemk30  31156  cdlemk31  31158  cdlemk39  31178  cdlemkfid1N  31183  cdlemkid1  31184  cdlemkid2  31186  cdlemkfid3N  31187  cdlemk19ylem  31192  cdlemk19xlem  31204  cdlemk19x  31205  cdlemk53b  31218  cdlemk53  31219  cdlemk54  31220  cdlemk55a  31221  cdlemk43N  31225  cdlemk19u1  31231  cdlemk19u  31232  cdleml1N  31238  erngdvlem4  31253  erngdvlem4-rN  31261  dia11N  31311  cdlemm10N  31381  dib11N  31423  cdlemn2  31458  cdlemn10  31469  dihjustlem  31479  dihord2cN  31484  dihlsscpre  31497  dih1dimb2  31504  dihvalcq2  31510  dihopelvalcpre  31511  dihord6b  31523  dih11  31528  dihmeetlem1N  31553  dihglblem2N  31557  dihglblem3N  31558  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetcN  31565  dihmeetbclemN  31567  dihmeetlem4preN  31569  dihmeetlem9N  31578  dihmeetlem20N  31589  dihlspsnssN  31595  dihlspsnat  31596  dihatlat  31597  dihglblem6  31603  dochss  31628  hdmapval3N  32104  hgmap11  32168
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator