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

Theorem simp1l 980
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 977 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  simpl1l  1007  simpr1l  1013  simp11l  1067  simp21l  1073  simp31l  1079  tfisi  4752  funprg  5404  omeulem2  6723  uniinqs  6881  unxpdomlem3  7212  elfiun  7330  cantnffval  7511  tcrank  7701  cofsmo  8042  isfin2-2  8092  tskint  8554  tskun  8555  tskurn  8558  gruina  8587  dmdcan  9617  lt2msq1  9786  supmullem1  9867  supmul  9869  xaddass  10721  xaddass2  10722  xlt2add  10732  xmulasslem3  10758  xadddi2r  10770  iccsplit  10921  expaddzlem  11310  expaddz  11311  expmulz  11313  ccatopth2  11664  resqrcl  11946  limsupgle  12158  o1add  12294  o1mul  12295  o1sub  12296  bitsfzo  12834  sadfval  12851  smufval  12876  prmexpb  13004  4sqlem18  13217  vdwlem10  13245  submre  13717  mrelatlub  14499  spwpr4  14550  mndodcong  15067  subgabl  15342  gex2abl  15353  cntzsubr  15787  abvres  15814  lbsind2  16044  lspsneu  16086  lbsextlem2  16122  lbsextg  16125  cnprest  17234  hausnei2  17298  isreg2  17322  cmpcld  17346  llyrest  17428  nllyrest  17429  csdfil  17802  hausflimlem  17887  ssbl  18184  dvres2  19477  plyadd  19814  plymul  19815  coeeu  19822  vieta1  19907  aalioulem3  19929  aalioulem4  19930  cxpadd  20248  cxpsub  20251  mulcxp  20254  divcxp  20256  cxple2  20266  cxplt2  20267  cxpcn3lem  20309  angcan  20322  ang180lem5  20333  isosctrlem3  20342  logexprlim  20687  abvcxp  20987  padicabv  21002  chscllem4  22653  dedekind  24756  poseq  25079  nofulllem5  25186  brbtwn2  25360  ax5seglem6  25389  axcontlem4  25422  axcontlem8  25426  ifscgr  25494  congtr  26643  fzmaxdif  26659  isnumbasgrplem2  26860  lindfind2  26879  matrng  27071  refsumcn  27292  fmuldfeq  27304  stoweidlem31  27371  stoweidlem34  27374  stoweidlem43  27383  stoweidlem46  27386  stoweidlem52  27392  stoweidlem53  27393  stoweidlem54  27394  stoweidlem55  27395  stoweidlem56  27396  stoweidlem57  27397  stoweidlem58  27398  stoweidlem59  27399  stoweidlem60  27400  stoweid  27403  stirlinglem13  27426  lshpnelb  29233  lfl1  29319  lshpkrlem6  29364  lshpkrex  29367  hlrelat3  29660  atbtwnexOLDN  29695  atbtwnex  29696  3dim3  29717  3atlem5  29735  2llnmat  29772  lvolex3N  29786  lvolnle3at  29830  4atlem11  29857  4atlem12  29860  dalemccea  29931  cdlema2N  30040  paddasslem2  30069  atmod1i1m  30106  lhp2lt  30249  lhp0lt  30251  lhpj1  30270  lhpmcvr4N  30274  lhpelim  30285  lhpmod2i2  30286  lhpmod6i1  30287  cdlemb2  30289  lhple  30290  lhpat  30291  4atex  30324  4atex2-0aOLDN  30326  4atex3  30329  ldilco  30364  ltrncl  30373  ltrn11  30374  ltrnle  30377  ltrncnvleN  30378  ltrnm  30379  ltrnj  30380  ltrncvr  30381  ltrnatb  30385  ltrnel  30387  ltrncnvel  30390  ltrncnv  30394  ltrnmw  30399  trlval2  30411  trlcnv  30413  trljat1  30414  trljat2  30415  trl0  30418  ltrnnidn  30422  trlnidatb  30425  cdlemc1  30439  cdlemc2  30440  cdlemc5  30443  cdlemc6  30444  cdlemd3  30448  cdlemd6  30451  cdleme0aa  30458  cdleme0b  30460  cdleme0c  30461  cdleme0e  30465  cdleme0fN  30466  cdleme01N  30469  cdleme02N  30470  cdleme0ex1N  30471  cdleme0moN  30473  cdleme3g  30482  cdleme3h  30483  cdleme3  30485  cdleme4  30486  cdleme4a  30487  cdleme5  30488  cdleme8  30498  cdleme9  30501  cdleme10  30502  cdleme16aN  30507  cdleme11a  30508  cdleme11fN  30512  cdleme11g  30513  cdleme11h  30514  cdleme11j  30515  cdleme11k  30516  cdleme12  30519  cdleme13  30520  cdleme17c  30536  cdleme17d1  30537  cdleme18a  30539  cdleme18b  30540  cdleme18c  30541  cdleme22gb  30542  cdlemeda  30546  cdlemednpq  30547  cdlemednuN  30548  cdleme19c  30553  cdleme20aN  30557  cdleme20bN  30558  cdleme20c  30559  cdleme22aa  30587  cdleme22a  30588  cdleme22b  30589  cdleme22d  30591  cdleme22e  30592  cdleme27cl  30614  cdleme27a  30615  cdleme30a  30626  cdleme42a  30719  cdleme42c  30720  cdleme50laut  30795  cdlemf1  30809  cdlemf  30811  cdlemfnid  30812  trlord  30817  cdlemg2fv2  30848  cdlemg2kq  30850  cdlemg2m  30852  cdlemg4a  30856  cdlemg4d  30861  cdlemg4g  30864  cdlemg4  30865  cdlemg6c  30868  cdlemg7aN  30873  cdlemg8a  30875  cdlemg8b  30876  cdlemg8c  30877  cdlemg9a  30880  cdlemg9b  30881  cdlemg9  30882  cdlemg11aq  30886  cdlemg10c  30887  cdlemg12a  30891  cdlemg12b  30892  cdlemg12c  30893  cdlemg17a  30909  cdlemg18b  30927  cdlemg18c  30928  cdlemg31b0a  30943  cdlemg31a  30945  cdlemg31b  30946  cdlemg31d  30948  cdlemg35  30961  trlcoabs2N  30970  trlcolem  30974  cdlemg44a  30979  trljco  30988  trljco2  30989  tendoco2  31016  tendopltp  31028  cdlemi1  31066  cdlemi2  31067  cdlemj3  31071  tendocan  31072  cdlemk3  31081  cdlemk4  31082  cdlemk5a  31083  cdlemk9  31087  cdlemk9bN  31088  cdlemkvcl  31090  cdlemk10  31091  cdlemk30  31142  cdlemk31  31144  cdlemk39  31164  cdlemkfid1N  31169  cdlemkid1  31170  cdlemkid2  31172  cdlemkfid3N  31173  cdlemk19ylem  31178  cdlemk19xlem  31190  cdlemk19x  31191  cdlemk53b  31204  cdlemk53  31205  cdlemk54  31206  cdlemk55a  31207  cdlemk43N  31211  cdlemk19u1  31217  cdlemk19u  31218  cdleml1N  31224  erngdvlem4  31239  erngdvlem4-rN  31247  dia11N  31297  cdlemm10N  31367  dib11N  31409  cdlemn2  31444  cdlemn10  31455  dihjustlem  31465  dihord2cN  31470  dihlsscpre  31483  dih1dimb2  31490  dihvalcq2  31496  dihopelvalcpre  31497  dihord6b  31509  dih11  31514  dihmeetlem1N  31539  dihglblem2N  31543  dihglblem3N  31544  dihmeetlem2N  31548  dihglbcpreN  31549  dihmeetcN  31551  dihmeetbclemN  31553  dihmeetlem4preN  31555  dihmeetlem9N  31564  dihmeetlem20N  31575  dihlspsnssN  31581  dihlspsnat  31582  dihatlat  31583  dihglblem6  31589  dochss  31614  hdmapval3N  32090  hgmap11  32154
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 937
  Copyright terms: Public domain W3C validator