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  4649  funprg  5301  omeulem2  6581  unxpdomlem3  7069  elfiun  7183  cantnffval  7364  tcrank  7554  cofsmo  7895  isfin2-2  7945  tskint  8407  tskun  8408  tskurn  8411  gruina  8440  dmdcan  9470  lt2msq1  9639  supmullem1  9720  supmul  9722  xaddass  10569  xaddass2  10570  xlt2add  10580  xmulasslem3  10606  xadddi2r  10618  iccsplit  10768  expaddzlem  11145  expaddz  11146  expmulz  11148  ccatopth2  11463  resqrcl  11739  limsupgle  11951  o1add  12087  o1mul  12088  o1sub  12089  bitsfzo  12626  sadfval  12643  smufval  12668  prmexpb  12796  4sqlem18  13009  vdwlem10  13037  submre  13507  mrelatlub  14289  spwpr4  14340  mndodcong  14857  subgabl  15132  gex2abl  15143  cntzsubr  15577  abvres  15604  lbsind2  15834  lspsneu  15876  lbsextlem2  15912  lbsextg  15915  cnprest  17017  hausnei2  17081  isreg2  17105  cmpcld  17129  llyrest  17211  nllyrest  17212  csdfil  17589  hausflimlem  17674  ssbl  17971  dvres2  19262  plyadd  19599  plymul  19600  coeeu  19607  vieta1  19692  aalioulem3  19714  aalioulem4  19715  cxpadd  20026  cxpsub  20029  mulcxp  20032  divcxp  20034  cxple2  20044  cxplt2  20045  cxpcn3lem  20087  angcan  20100  ang180lem5  20111  isosctrlem3  20120  logexprlim  20464  abvcxp  20764  padicabv  20779  chscllem4  22219  dedekind  24082  poseq  24253  nofulllem5  24360  brbtwn2  24533  ax5seglem6  24562  axcontlem4  24595  axcontlem8  24599  ifscgr  24667  uninqs  25039  intopcoaconlem3b  25538  prdnei  25573  islimrs  25580  flfneic  25624  setiscat  25979  congtr  27052  fzmaxdif  27068  isnumbasgrplem2  27269  lindfind2  27288  matrng  27480  refsumcn  27701  fmuldfeq  27713  stoweidlem31  27780  stoweidlem34  27783  stoweidlem43  27792  stoweidlem46  27795  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem55  27804  stoweidlem56  27805  stoweidlem57  27806  stoweidlem58  27807  stoweidlem59  27808  stoweidlem60  27809  stoweid  27812  stirlinglem13  27835  lshpnelb  29174  lfl1  29260  lshpkrlem6  29305  lshpkrex  29308  hlrelat3  29601  atbtwnexOLDN  29636  atbtwnex  29637  3dim3  29658  3atlem5  29676  2llnmat  29713  lvolex3N  29727  lvolnle3at  29771  4atlem11  29798  4atlem12  29801  dalemccea  29872  cdlema2N  29981  paddasslem2  30010  atmod1i1m  30047  lhp2lt  30190  lhp0lt  30192  lhpj1  30211  lhpmcvr4N  30215  lhpelim  30226  lhpmod2i2  30227  lhpmod6i1  30228  cdlemb2  30230  lhple  30231  lhpat  30232  4atex  30265  4atex2-0aOLDN  30267  4atex3  30270  ldilco  30305  ltrncl  30314  ltrn11  30315  ltrnle  30318  ltrncnvleN  30319  ltrnm  30320  ltrnj  30321  ltrncvr  30322  ltrnatb  30326  ltrnel  30328  ltrncnvel  30331  ltrncnv  30335  ltrnmw  30340  trlval2  30352  trlcnv  30354  trljat1  30355  trljat2  30356  trl0  30359  ltrnnidn  30363  trlnidatb  30366  cdlemc1  30380  cdlemc2  30381  cdlemc5  30384  cdlemc6  30385  cdlemd3  30389  cdlemd6  30392  cdleme0aa  30399  cdleme0b  30401  cdleme0c  30402  cdleme0e  30406  cdleme0fN  30407  cdleme01N  30410  cdleme02N  30411  cdleme0ex1N  30412  cdleme0moN  30414  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme4  30427  cdleme4a  30428  cdleme5  30429  cdleme8  30439  cdleme9  30442  cdleme10  30443  cdleme16aN  30448  cdleme11a  30449  cdleme11fN  30453  cdleme11g  30454  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme12  30460  cdleme13  30461  cdleme17c  30477  cdleme17d1  30478  cdleme18a  30480  cdleme18b  30481  cdleme18c  30482  cdleme22gb  30483  cdlemeda  30487  cdlemednpq  30488  cdlemednuN  30489  cdleme19c  30494  cdleme20aN  30498  cdleme20bN  30499  cdleme20c  30500  cdleme22aa  30528  cdleme22a  30529  cdleme22b  30530  cdleme22d  30532  cdleme22e  30533  cdleme27cl  30555  cdleme27a  30556  cdleme30a  30567  cdleme42a  30660  cdleme42c  30661  cdleme50laut  30736  cdlemf1  30750  cdlemf  30752  cdlemfnid  30753  trlord  30758  cdlemg2fv2  30789  cdlemg2kq  30791  cdlemg2m  30793  cdlemg4a  30797  cdlemg4d  30802  cdlemg4g  30805  cdlemg4  30806  cdlemg6c  30809  cdlemg7aN  30814  cdlemg8a  30816  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg9b  30822  cdlemg9  30823  cdlemg11aq  30827  cdlemg10c  30828  cdlemg12a  30832  cdlemg12b  30833  cdlemg12c  30834  cdlemg17a  30850  cdlemg18b  30868  cdlemg18c  30869  cdlemg31b0a  30884  cdlemg31a  30886  cdlemg31b  30887  cdlemg31d  30889  cdlemg35  30902  trlcoabs2N  30911  trlcolem  30915  cdlemg44a  30920  trljco  30929  trljco2  30930  tendoco2  30957  tendopltp  30969  cdlemi1  31007  cdlemi2  31008  cdlemj3  31012  tendocan  31013  cdlemk3  31022  cdlemk4  31023  cdlemk5a  31024  cdlemk9  31028  cdlemk9bN  31029  cdlemkvcl  31031  cdlemk10  31032  cdlemk30  31083  cdlemk31  31085  cdlemk39  31105  cdlemkfid1N  31110  cdlemkid1  31111  cdlemkid2  31113  cdlemkfid3N  31114  cdlemk19ylem  31119  cdlemk19xlem  31131  cdlemk19x  31132  cdlemk53b  31145  cdlemk53  31146  cdlemk54  31147  cdlemk55a  31148  cdlemk43N  31152  cdlemk19u1  31158  cdlemk19u  31159  cdleml1N  31165  erngdvlem4  31180  erngdvlem4-rN  31188  dia11N  31238  cdlemm10N  31308  dib11N  31350  cdlemn2  31385  cdlemn10  31396  dihjustlem  31406  dihord2cN  31411  dihlsscpre  31424  dih1dimb2  31431  dihvalcq2  31437  dihopelvalcpre  31438  dihord6b  31450  dih11  31455  dihmeetlem1N  31480  dihglblem2N  31484  dihglblem3N  31485  dihmeetlem2N  31489  dihglbcpreN  31490  dihmeetcN  31492  dihmeetbclemN  31494  dihmeetlem4preN  31496  dihmeetlem9N  31505  dihmeetlem20N  31516  dihlspsnssN  31522  dihlspsnat  31523  dihatlat  31524  dihglblem6  31530  dochss  31555  hdmapval3N  32031  hgmap11  32095
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