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  4665  funprg  5317  omeulem2  6597  unxpdomlem3  7085  elfiun  7199  cantnffval  7380  tcrank  7570  cofsmo  7911  isfin2-2  7961  tskint  8423  tskun  8424  tskurn  8427  gruina  8456  dmdcan  9486  lt2msq1  9655  supmullem1  9736  supmul  9738  xaddass  10585  xaddass2  10586  xlt2add  10596  xmulasslem3  10622  xadddi2r  10634  iccsplit  10784  expaddzlem  11161  expaddz  11162  expmulz  11164  ccatopth2  11479  resqrcl  11755  limsupgle  11967  o1add  12103  o1mul  12104  o1sub  12105  bitsfzo  12642  sadfval  12659  smufval  12684  prmexpb  12812  4sqlem18  13025  vdwlem10  13053  submre  13523  mrelatlub  14305  spwpr4  14356  mndodcong  14873  subgabl  15148  gex2abl  15159  cntzsubr  15593  abvres  15620  lbsind2  15850  lspsneu  15892  lbsextlem2  15928  lbsextg  15931  cnprest  17033  hausnei2  17097  isreg2  17121  cmpcld  17145  llyrest  17227  nllyrest  17228  csdfil  17605  hausflimlem  17690  ssbl  17987  dvres2  19278  plyadd  19615  plymul  19616  coeeu  19623  vieta1  19708  aalioulem3  19730  aalioulem4  19731  cxpadd  20042  cxpsub  20045  mulcxp  20048  divcxp  20050  cxple2  20060  cxplt2  20061  cxpcn3lem  20103  angcan  20116  ang180lem5  20127  isosctrlem3  20136  logexprlim  20480  abvcxp  20780  padicabv  20795  chscllem4  22235  dedekind  24097  poseq  24324  nofulllem5  24431  brbtwn2  24605  ax5seglem6  24634  axcontlem4  24667  axcontlem8  24671  ifscgr  24739  uninqs  25142  intopcoaconlem3b  25641  prdnei  25676  islimrs  25683  flfneic  25727  setiscat  26082  congtr  27155  fzmaxdif  27171  isnumbasgrplem2  27372  lindfind2  27391  matrng  27583  refsumcn  27804  fmuldfeq  27816  stoweidlem31  27883  stoweidlem34  27886  stoweidlem43  27895  stoweidlem46  27898  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  stoweidlem55  27907  stoweidlem56  27908  stoweidlem57  27909  stoweidlem58  27910  stoweidlem59  27911  stoweidlem60  27912  stoweid  27915  stirlinglem13  27938  lshpnelb  29796  lfl1  29882  lshpkrlem6  29927  lshpkrex  29930  hlrelat3  30223  atbtwnexOLDN  30258  atbtwnex  30259  3dim3  30280  3atlem5  30298  2llnmat  30335  lvolex3N  30349  lvolnle3at  30393  4atlem11  30420  4atlem12  30423  dalemccea  30494  cdlema2N  30603  paddasslem2  30632  atmod1i1m  30669  lhp2lt  30812  lhp0lt  30814  lhpj1  30833  lhpmcvr4N  30837  lhpelim  30848  lhpmod2i2  30849  lhpmod6i1  30850  cdlemb2  30852  lhple  30853  lhpat  30854  4atex  30887  4atex2-0aOLDN  30889  4atex3  30892  ldilco  30927  ltrncl  30936  ltrn11  30937  ltrnle  30940  ltrncnvleN  30941  ltrnm  30942  ltrnj  30943  ltrncvr  30944  ltrnatb  30948  ltrnel  30950  ltrncnvel  30953  ltrncnv  30957  ltrnmw  30962  trlval2  30974  trlcnv  30976  trljat1  30977  trljat2  30978  trl0  30981  ltrnnidn  30985  trlnidatb  30988  cdlemc1  31002  cdlemc2  31003  cdlemc5  31006  cdlemc6  31007  cdlemd3  31011  cdlemd6  31014  cdleme0aa  31021  cdleme0b  31023  cdleme0c  31024  cdleme0e  31028  cdleme0fN  31029  cdleme01N  31032  cdleme02N  31033  cdleme0ex1N  31034  cdleme0moN  31036  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme4  31049  cdleme4a  31050  cdleme5  31051  cdleme8  31061  cdleme9  31064  cdleme10  31065  cdleme16aN  31070  cdleme11a  31071  cdleme11fN  31075  cdleme11g  31076  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme12  31082  cdleme13  31083  cdleme17c  31099  cdleme17d1  31100  cdleme18a  31102  cdleme18b  31103  cdleme18c  31104  cdleme22gb  31105  cdlemeda  31109  cdlemednpq  31110  cdlemednuN  31111  cdleme19c  31116  cdleme20aN  31120  cdleme20bN  31121  cdleme20c  31122  cdleme22aa  31150  cdleme22a  31151  cdleme22b  31152  cdleme22d  31154  cdleme22e  31155  cdleme27cl  31177  cdleme27a  31178  cdleme30a  31189  cdleme42a  31282  cdleme42c  31283  cdleme50laut  31358  cdlemf1  31372  cdlemf  31374  cdlemfnid  31375  trlord  31380  cdlemg2fv2  31411  cdlemg2kq  31413  cdlemg2m  31415  cdlemg4a  31419  cdlemg4d  31424  cdlemg4g  31427  cdlemg4  31428  cdlemg6c  31431  cdlemg7aN  31436  cdlemg8a  31438  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg9b  31444  cdlemg9  31445  cdlemg11aq  31449  cdlemg10c  31450  cdlemg12a  31454  cdlemg12b  31455  cdlemg12c  31456  cdlemg17a  31472  cdlemg18b  31490  cdlemg18c  31491  cdlemg31b0a  31506  cdlemg31a  31508  cdlemg31b  31509  cdlemg31d  31511  cdlemg35  31524  trlcoabs2N  31533  trlcolem  31537  cdlemg44a  31542  trljco  31551  trljco2  31552  tendoco2  31579  tendopltp  31591  cdlemi1  31629  cdlemi2  31630  cdlemj3  31634  tendocan  31635  cdlemk3  31644  cdlemk4  31645  cdlemk5a  31646  cdlemk9  31650  cdlemk9bN  31651  cdlemkvcl  31653  cdlemk10  31654  cdlemk30  31705  cdlemk31  31707  cdlemk39  31727  cdlemkfid1N  31732  cdlemkid1  31733  cdlemkid2  31735  cdlemkfid3N  31736  cdlemk19ylem  31741  cdlemk19xlem  31753  cdlemk19x  31754  cdlemk53b  31767  cdlemk53  31768  cdlemk54  31769  cdlemk55a  31770  cdlemk43N  31774  cdlemk19u1  31780  cdlemk19u  31781  cdleml1N  31787  erngdvlem4  31802  erngdvlem4-rN  31810  dia11N  31860  cdlemm10N  31930  dib11N  31972  cdlemn2  32007  cdlemn10  32018  dihjustlem  32028  dihord2cN  32033  dihlsscpre  32046  dih1dimb2  32053  dihvalcq2  32059  dihopelvalcpre  32060  dihord6b  32072  dih11  32077  dihmeetlem1N  32102  dihglblem2N  32106  dihglblem3N  32107  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetcN  32114  dihmeetbclemN  32116  dihmeetlem4preN  32118  dihmeetlem9N  32127  dihmeetlem20N  32138  dihlspsnssN  32144  dihlspsnat  32145  dihatlat  32146  dihglblem6  32152  dochss  32177  hdmapval3N  32653  hgmap11  32717
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