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

Theorem simp1l 1029
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 458 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 1026 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl1l  1056  simpr1l  1062  simp11l  1116  simp21l  1122  simp31l  1128  funprg  5650  tfisi  6699  omeulem2  7292  uniinqs  7451  unxpdomlem3  7784  elfiun  7950  cantnffval  8167  tcrank  8354  cofsmo  8697  isfin2-2  8747  tskint  9209  tskun  9210  tskurn  9213  gruina  9242  dedekind  9796  dmdcan  10316  lt2msq1  10489  supmullem1  10577  supmul  10579  xaddass  11535  xaddass2  11536  xlt2add  11546  xmulasslem3  11572  xadddi2r  11584  iccsplit  11763  expaddzlem  12312  expaddz  12313  expmulz  12315  ccatopth2  12812  swrdccat3  12833  resqrtcl  13296  limsupgle  13513  o1add  13655  o1mul  13656  o1sub  13657  bitsfzo  14383  sadfval  14400  smufval  14425  prmexpb  14641  4sqlem18OLD  14869  4sqlem18  14875  vdwlem10  14903  fsets  15112  submre  15462  mrelatlub  16383  mndodcong  17133  subgabl  17411  gex2abl  17424  cntzsubr  17975  abvres  18002  lbsind2  18239  lspsneu  18281  lbsextlem2  18317  lbsextg  18320  lindfind2  19307  matring  19399  maducoeval  19595  maducoeval2  19596  maduf  19597  madurid  19600  gsummatr01  19615  cramerimplem3  19641  cnprest  20236  hausnei2  20300  isreg2  20324  cmpcld  20348  llyrest  20431  nllyrest  20432  csdfil  20840  hausflimlem  20925  ssblps  21368  ssbl  21369  dvres2  22744  plyadd  23039  plymul  23040  coeeu  23047  vieta1  23133  aalioulem3  23155  aalioulem4  23156  efgh  23355  cxpadd  23489  cxpsub  23492  mulcxp  23495  divcxp  23497  cxple2  23507  cxplt2  23508  cxpcn3lem  23552  angcan  23596  ang180lem5  23607  isosctrlem3  23614  logexprlim  24016  abvcxp  24316  padicabv  24331  brbtwn2  24781  ax5seglem6  24810  axcontlem4  24843  axcontlem8  24847  clwwlknimp  25349  chscllem4  27128  ogrpinvlt  28325  poseq  30278  wsuclem  30295  nofulllem5  30380  ifscgr  30596  lshpnelb  32259  lfl1  32345  lshpkrlem6  32390  lshpkrex  32393  hlrelat3  32686  atbtwnexOLDN  32721  atbtwnex  32722  3dim3  32743  3atlem5  32761  2llnmat  32798  lvolex3N  32812  lvolnle3at  32856  4atlem11  32883  4atlem12  32886  dalemccea  32957  cdlema2N  33066  paddasslem2  33095  atmod1i1m  33132  lhp2lt  33275  lhp0lt  33277  lhpj1  33296  lhpmcvr4N  33300  lhpelim  33311  lhpmod2i2  33312  lhpmod6i1  33313  cdlemb2  33315  lhple  33316  lhpat  33317  4atex  33350  4atex2-0aOLDN  33352  4atex3  33355  ldilco  33390  ltrncl  33399  ltrn11  33400  ltrnle  33403  ltrncnvleN  33404  ltrnm  33405  ltrnj  33406  ltrncvr  33407  ltrnatb  33411  ltrnel  33413  ltrncnvel  33416  ltrncnv  33420  ltrnmwOLD  33426  trlval2  33438  trlcnv  33440  trljat1  33441  trljat2  33442  trl0  33445  ltrnnidn  33449  trlnidatb  33452  cdlemc1  33466  cdlemc2  33467  cdlemc5  33470  cdlemc6  33471  cdlemd3  33475  cdlemd6  33478  cdleme0aa  33485  cdleme0b  33487  cdleme0c  33488  cdleme0e  33492  cdleme0fN  33493  cdleme01N  33496  cdleme02N  33497  cdleme0ex1N  33498  cdleme0moN  33500  cdleme3g  33509  cdleme3h  33510  cdleme3  33512  cdleme4  33513  cdleme4a  33514  cdleme5  33515  cdleme8  33525  cdleme9  33528  cdleme10  33529  cdleme16aN  33534  cdleme11a  33535  cdleme11fN  33539  cdleme11g  33540  cdleme11h  33541  cdleme11j  33542  cdleme11k  33543  cdleme12  33546  cdleme13  33547  cdleme17c  33563  cdleme17d1  33564  cdleme18a  33566  cdleme18b  33567  cdleme18c  33568  cdleme22gb  33569  cdlemeda  33573  cdlemednpq  33574  cdlemednuN  33575  cdleme19c  33581  cdleme20aN  33585  cdleme20bN  33586  cdleme20c  33587  cdleme22aa  33615  cdleme22a  33616  cdleme22b  33617  cdleme22d  33619  cdleme22e  33620  cdleme27cl  33642  cdleme27a  33643  cdleme30a  33654  cdleme42a  33747  cdleme42c  33748  cdleme50laut  33823  cdlemf1  33837  cdlemf  33839  cdlemfnid  33840  trlord  33845  cdlemg2fv2  33876  cdlemg2kq  33878  cdlemg2m  33880  cdlemg4a  33884  cdlemg4d  33889  cdlemg4g  33892  cdlemg4  33893  cdlemg6c  33896  cdlemg7aN  33901  cdlemg8a  33903  cdlemg8b  33904  cdlemg8c  33905  cdlemg9a  33908  cdlemg9b  33909  cdlemg9  33910  cdlemg11aq  33914  cdlemg10c  33915  cdlemg12a  33919  cdlemg12b  33920  cdlemg12c  33921  cdlemg17a  33937  cdlemg18b  33955  cdlemg18c  33956  cdlemg31b0a  33971  cdlemg31a  33973  cdlemg31b  33974  cdlemg31d  33976  cdlemg35  33989  trlcoabs2N  33998  trlcolem  34002  cdlemg44a  34007  trljco  34016  trljco2  34017  tendoco2  34044  tendopltp  34056  cdlemi1  34094  cdlemi2  34095  cdlemj3  34099  tendocan  34100  cdlemk3  34109  cdlemk4  34110  cdlemk5a  34111  cdlemk9  34115  cdlemk9bN  34116  cdlemkvcl  34118  cdlemk10  34119  cdlemk30  34170  cdlemk31  34172  cdlemk39  34192  cdlemkfid1N  34197  cdlemkid1  34198  cdlemkid2  34200  cdlemkfid3N  34201  cdlemk19ylem  34206  cdlemk19xlem  34218  cdlemk19x  34219  cdlemk53b  34232  cdlemk53  34233  cdlemk54  34234  cdlemk55a  34235  cdlemk43N  34239  cdlemk19u1  34245  cdlemk19u  34246  cdleml1N  34252  erngdvlem4  34267  erngdvlem4-rN  34275  dia11N  34325  cdlemm10N  34395  dib11N  34437  cdlemn2  34472  cdlemn10  34483  dihjustlem  34493  dihord2cN  34498  dihlsscpre  34511  dih1dimb2  34518  dihvalcq2  34524  dihopelvalcpre  34525  dihord6b  34537  dih11  34542  dihmeetlem1N  34567  dihglblem2N  34571  dihglblem3N  34572  dihmeetlem2N  34576  dihglbcpreN  34577  dihmeetcN  34579  dihmeetbclemN  34581  dihmeetlem4preN  34583  dihmeetlem9N  34592  dihmeetlem20N  34603  dihlspsnssN  34609  dihlspsnat  34610  dihatlat  34611  dihglblem6  34617  dihmeet  34620  dochss  34642  hdmapval3N  35118  hgmap11  35182  congtr  35521  fzmaxdif  35537  isnumbasgrplem2  35669  mullimc  37268  mullimcf  37275  islpcn  37291  cncfuni  37336  icccncfext  37337  stoweidlem34  37464  stoweidlem59  37489  stirlinglem13  37517  fourierdlem41  37579  fourierdlem42  37580  fourierdlem73  37611  sge0iunmptlemfi  37789  meadjiunlem  37812  pfxccat3  38357  lincscm  38983  lincext3  39009  el0ldep  39019  el0ldepsnzr  39020
  Copyright terms: Public domain W3C validator