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

Theorem simp1l 981
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 444 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl1l  1008  simpr1l  1014  simp11l  1068  simp21l  1074  simp31l  1080  tfisi  4797  funprg  5459  omeulem2  6785  uniinqs  6943  unxpdomlem3  7274  elfiun  7393  cantnffval  7574  tcrank  7764  cofsmo  8105  isfin2-2  8155  tskint  8616  tskun  8617  tskurn  8620  gruina  8649  dmdcan  9680  lt2msq1  9849  supmullem1  9930  supmul  9932  xaddass  10784  xaddass2  10785  xlt2add  10795  xmulasslem3  10821  xadddi2r  10833  iccsplit  10985  expaddzlem  11378  expaddz  11379  expmulz  11381  ccatopth2  11732  resqrcl  12014  limsupgle  12226  o1add  12362  o1mul  12363  o1sub  12364  bitsfzo  12902  sadfval  12919  smufval  12944  prmexpb  13072  4sqlem18  13285  vdwlem10  13313  submre  13785  mrelatlub  14567  spwpr4  14618  mndodcong  15135  subgabl  15410  gex2abl  15421  cntzsubr  15855  abvres  15882  lbsind2  16108  lspsneu  16150  lbsextlem2  16186  lbsextg  16189  cnprest  17307  hausnei2  17371  isreg2  17395  cmpcld  17419  llyrest  17501  nllyrest  17502  csdfil  17879  hausflimlem  17964  ssblps  18405  ssbl  18406  dvres2  19752  plyadd  20089  plymul  20090  coeeu  20097  vieta1  20182  aalioulem3  20204  aalioulem4  20205  cxpadd  20523  cxpsub  20526  mulcxp  20529  divcxp  20531  cxple2  20541  cxplt2  20542  cxpcn3lem  20584  angcan  20597  ang180lem5  20608  isosctrlem3  20617  logexprlim  20962  abvcxp  21262  padicabv  21277  chscllem4  23095  dedekind  25140  poseq  25467  nofulllem5  25574  brbtwn2  25748  ax5seglem6  25777  axcontlem4  25810  axcontlem8  25814  ifscgr  25882  congtr  26920  fzmaxdif  26936  isnumbasgrplem2  27137  lindfind2  27156  matrng  27348  stoweidlem34  27650  stoweidlem59  27675  stirlinglem13  27702  swrdccat3  28029  lshpnelb  29467  lfl1  29553  lshpkrlem6  29598  lshpkrex  29601  hlrelat3  29894  atbtwnexOLDN  29929  atbtwnex  29930  3dim3  29951  3atlem5  29969  2llnmat  30006  lvolex3N  30020  lvolnle3at  30064  4atlem11  30091  4atlem12  30094  dalemccea  30165  cdlema2N  30274  paddasslem2  30303  atmod1i1m  30340  lhp2lt  30483  lhp0lt  30485  lhpj1  30504  lhpmcvr4N  30508  lhpelim  30519  lhpmod2i2  30520  lhpmod6i1  30521  cdlemb2  30523  lhple  30524  lhpat  30525  4atex  30558  4atex2-0aOLDN  30560  4atex3  30563  ldilco  30598  ltrncl  30607  ltrn11  30608  ltrnle  30611  ltrncnvleN  30612  ltrnm  30613  ltrnj  30614  ltrncvr  30615  ltrnatb  30619  ltrnel  30621  ltrncnvel  30624  ltrncnv  30628  ltrnmw  30633  trlval2  30645  trlcnv  30647  trljat1  30648  trljat2  30649  trl0  30652  ltrnnidn  30656  trlnidatb  30659  cdlemc1  30673  cdlemc2  30674  cdlemc5  30677  cdlemc6  30678  cdlemd3  30682  cdlemd6  30685  cdleme0aa  30692  cdleme0b  30694  cdleme0c  30695  cdleme0e  30699  cdleme0fN  30700  cdleme01N  30703  cdleme02N  30704  cdleme0ex1N  30705  cdleme0moN  30707  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme4  30720  cdleme4a  30721  cdleme5  30722  cdleme8  30732  cdleme9  30735  cdleme10  30736  cdleme16aN  30741  cdleme11a  30742  cdleme11fN  30746  cdleme11g  30747  cdleme11h  30748  cdleme11j  30749  cdleme11k  30750  cdleme12  30753  cdleme13  30754  cdleme17c  30770  cdleme17d1  30771  cdleme18a  30773  cdleme18b  30774  cdleme18c  30775  cdleme22gb  30776  cdlemeda  30780  cdlemednpq  30781  cdlemednuN  30782  cdleme19c  30787  cdleme20aN  30791  cdleme20bN  30792  cdleme20c  30793  cdleme22aa  30821  cdleme22a  30822  cdleme22b  30823  cdleme22d  30825  cdleme22e  30826  cdleme27cl  30848  cdleme27a  30849  cdleme30a  30860  cdleme42a  30953  cdleme42c  30954  cdleme50laut  31029  cdlemf1  31043  cdlemf  31045  cdlemfnid  31046  trlord  31051  cdlemg2fv2  31082  cdlemg2kq  31084  cdlemg2m  31086  cdlemg4a  31090  cdlemg4d  31095  cdlemg4g  31098  cdlemg4  31099  cdlemg6c  31102  cdlemg7aN  31107  cdlemg8a  31109  cdlemg8b  31110  cdlemg8c  31111  cdlemg9a  31114  cdlemg9b  31115  cdlemg9  31116  cdlemg11aq  31120  cdlemg10c  31121  cdlemg12a  31125  cdlemg12b  31126  cdlemg12c  31127  cdlemg17a  31143  cdlemg18b  31161  cdlemg18c  31162  cdlemg31b0a  31177  cdlemg31a  31179  cdlemg31b  31180  cdlemg31d  31182  cdlemg35  31195  trlcoabs2N  31204  trlcolem  31208  cdlemg44a  31213  trljco  31222  trljco2  31223  tendoco2  31250  tendopltp  31262  cdlemi1  31300  cdlemi2  31301  cdlemj3  31305  tendocan  31306  cdlemk3  31315  cdlemk4  31316  cdlemk5a  31317  cdlemk9  31321  cdlemk9bN  31322  cdlemkvcl  31324  cdlemk10  31325  cdlemk30  31376  cdlemk31  31378  cdlemk39  31398  cdlemkfid1N  31403  cdlemkid1  31404  cdlemkid2  31406  cdlemkfid3N  31407  cdlemk19ylem  31412  cdlemk19xlem  31424  cdlemk19x  31425  cdlemk53b  31438  cdlemk53  31439  cdlemk54  31440  cdlemk55a  31441  cdlemk43N  31445  cdlemk19u1  31451  cdlemk19u  31452  cdleml1N  31458  erngdvlem4  31473  erngdvlem4-rN  31481  dia11N  31531  cdlemm10N  31601  dib11N  31643  cdlemn2  31678  cdlemn10  31689  dihjustlem  31699  dihord2cN  31704  dihlsscpre  31717  dih1dimb2  31724  dihvalcq2  31730  dihopelvalcpre  31731  dihord6b  31743  dih11  31748  dihmeetlem1N  31773  dihglblem2N  31777  dihglblem3N  31778  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetcN  31785  dihmeetbclemN  31787  dihmeetlem4preN  31789  dihmeetlem9N  31798  dihmeetlem20N  31809  dihlspsnssN  31815  dihlspsnat  31816  dihatlat  31817  dihglblem6  31823  dochss  31848  hdmapval3N  32324  hgmap11  32388
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator