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

Theorem simp1l 982
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 445 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 979 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simpl1l  1009  simpr1l  1015  simp11l  1069  simp21l  1075  simp31l  1081  tfisi  4840  funprg  5502  omeulem2  6828  uniinqs  6986  unxpdomlem3  7317  elfiun  7437  cantnffval  7620  tcrank  7810  cofsmo  8151  isfin2-2  8201  tskint  8662  tskun  8663  tskurn  8666  gruina  8695  dmdcan  9726  lt2msq1  9895  supmullem1  9976  supmul  9978  xaddass  10830  xaddass2  10831  xlt2add  10841  xmulasslem3  10867  xadddi2r  10879  iccsplit  11031  expaddzlem  11425  expaddz  11426  expmulz  11428  ccatopth2  11779  resqrcl  12061  limsupgle  12273  o1add  12409  o1mul  12410  o1sub  12411  bitsfzo  12949  sadfval  12966  smufval  12991  prmexpb  13119  4sqlem18  13332  vdwlem10  13360  submre  13832  mrelatlub  14614  spwpr4  14665  mndodcong  15182  subgabl  15457  gex2abl  15468  cntzsubr  15902  abvres  15929  lbsind2  16155  lspsneu  16197  lbsextlem2  16233  lbsextg  16236  cnprest  17355  hausnei2  17419  isreg2  17443  cmpcld  17467  llyrest  17550  nllyrest  17551  csdfil  17928  hausflimlem  18013  ssblps  18454  ssbl  18455  dvres2  19801  plyadd  20138  plymul  20139  coeeu  20146  vieta1  20231  aalioulem3  20253  aalioulem4  20254  cxpadd  20572  cxpsub  20575  mulcxp  20578  divcxp  20580  cxple2  20590  cxplt2  20591  cxpcn3lem  20633  angcan  20646  ang180lem5  20657  isosctrlem3  20666  logexprlim  21011  abvcxp  21311  padicabv  21326  chscllem4  23144  dedekind  25189  poseq  25530  wsuclem  25578  nofulllem5  25663  brbtwn2  25846  ax5seglem6  25875  axcontlem4  25908  axcontlem8  25912  ifscgr  25980  congtr  27032  fzmaxdif  27048  isnumbasgrplem2  27248  lindfind2  27267  matrng  27459  stoweidlem34  27761  stoweidlem59  27786  stirlinglem13  27813  swrdccat3  28237  lshpnelb  29844  lfl1  29930  lshpkrlem6  29975  lshpkrex  29978  hlrelat3  30271  atbtwnexOLDN  30306  atbtwnex  30307  3dim3  30328  3atlem5  30346  2llnmat  30383  lvolex3N  30397  lvolnle3at  30441  4atlem11  30468  4atlem12  30471  dalemccea  30542  cdlema2N  30651  paddasslem2  30680  atmod1i1m  30717  lhp2lt  30860  lhp0lt  30862  lhpj1  30881  lhpmcvr4N  30885  lhpelim  30896  lhpmod2i2  30897  lhpmod6i1  30898  cdlemb2  30900  lhple  30901  lhpat  30902  4atex  30935  4atex2-0aOLDN  30937  4atex3  30940  ldilco  30975  ltrncl  30984  ltrn11  30985  ltrnle  30988  ltrncnvleN  30989  ltrnm  30990  ltrnj  30991  ltrncvr  30992  ltrnatb  30996  ltrnel  30998  ltrncnvel  31001  ltrncnv  31005  ltrnmw  31010  trlval2  31022  trlcnv  31024  trljat1  31025  trljat2  31026  trl0  31029  ltrnnidn  31033  trlnidatb  31036  cdlemc1  31050  cdlemc2  31051  cdlemc5  31054  cdlemc6  31055  cdlemd3  31059  cdlemd6  31062  cdleme0aa  31069  cdleme0b  31071  cdleme0c  31072  cdleme0e  31076  cdleme0fN  31077  cdleme01N  31080  cdleme02N  31081  cdleme0ex1N  31082  cdleme0moN  31084  cdleme3g  31093  cdleme3h  31094  cdleme3  31096  cdleme4  31097  cdleme4a  31098  cdleme5  31099  cdleme8  31109  cdleme9  31112  cdleme10  31113  cdleme16aN  31118  cdleme11a  31119  cdleme11fN  31123  cdleme11g  31124  cdleme11h  31125  cdleme11j  31126  cdleme11k  31127  cdleme12  31130  cdleme13  31131  cdleme17c  31147  cdleme17d1  31148  cdleme18a  31150  cdleme18b  31151  cdleme18c  31152  cdleme22gb  31153  cdlemeda  31157  cdlemednpq  31158  cdlemednuN  31159  cdleme19c  31164  cdleme20aN  31168  cdleme20bN  31169  cdleme20c  31170  cdleme22aa  31198  cdleme22a  31199  cdleme22b  31200  cdleme22d  31202  cdleme22e  31203  cdleme27cl  31225  cdleme27a  31226  cdleme30a  31237  cdleme42a  31330  cdleme42c  31331  cdleme50laut  31406  cdlemf1  31420  cdlemf  31422  cdlemfnid  31423  trlord  31428  cdlemg2fv2  31459  cdlemg2kq  31461  cdlemg2m  31463  cdlemg4a  31467  cdlemg4d  31472  cdlemg4g  31475  cdlemg4  31476  cdlemg6c  31479  cdlemg7aN  31484  cdlemg8a  31486  cdlemg8b  31487  cdlemg8c  31488  cdlemg9a  31491  cdlemg9b  31492  cdlemg9  31493  cdlemg11aq  31497  cdlemg10c  31498  cdlemg12a  31502  cdlemg12b  31503  cdlemg12c  31504  cdlemg17a  31520  cdlemg18b  31538  cdlemg18c  31539  cdlemg31b0a  31554  cdlemg31a  31556  cdlemg31b  31557  cdlemg31d  31559  cdlemg35  31572  trlcoabs2N  31581  trlcolem  31585  cdlemg44a  31590  trljco  31599  trljco2  31600  tendoco2  31627  tendopltp  31639  cdlemi1  31677  cdlemi2  31678  cdlemj3  31682  tendocan  31683  cdlemk3  31692  cdlemk4  31693  cdlemk5a  31694  cdlemk9  31698  cdlemk9bN  31699  cdlemkvcl  31701  cdlemk10  31702  cdlemk30  31753  cdlemk31  31755  cdlemk39  31775  cdlemkfid1N  31780  cdlemkid1  31781  cdlemkid2  31783  cdlemkfid3N  31784  cdlemk19ylem  31789  cdlemk19xlem  31801  cdlemk19x  31802  cdlemk53b  31815  cdlemk53  31816  cdlemk54  31817  cdlemk55a  31818  cdlemk43N  31822  cdlemk19u1  31828  cdlemk19u  31829  cdleml1N  31835  erngdvlem4  31850  erngdvlem4-rN  31858  dia11N  31908  cdlemm10N  31978  dib11N  32020  cdlemn2  32055  cdlemn10  32066  dihjustlem  32076  dihord2cN  32081  dihlsscpre  32094  dih1dimb2  32101  dihvalcq2  32107  dihopelvalcpre  32108  dihord6b  32120  dih11  32125  dihmeetlem1N  32150  dihglblem2N  32154  dihglblem3N  32155  dihmeetlem2N  32159  dihglbcpreN  32160  dihmeetcN  32162  dihmeetbclemN  32164  dihmeetlem4preN  32166  dihmeetlem9N  32175  dihmeetlem20N  32186  dihlspsnssN  32192  dihlspsnat  32193  dihatlat  32194  dihglblem6  32200  dochss  32225  hdmapval3N  32701  hgmap11  32765
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator