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

Theorem simp1l 1054
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 464 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 1051 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  simpl1l  1081  simpr1l  1087  simp11l  1141  simp21l  1147  simp31l  1153  funprg  5638  tfisi  6704  omeulem2  7302  uniinqs  7461  unxpdomlem3  7796  elfiun  7962  cantnffval  8186  tcrank  8373  cofsmo  8717  isfin2-2  8767  tskint  9228  tskun  9229  tskurn  9232  gruina  9261  dedekind  9815  dmdcan  10339  lt2msq1  10512  supmullem1  10599  supmul  10601  xaddass  11560  xaddass2  11561  xlt2add  11571  xmulasslem3  11597  xadddi2r  11609  iccsplit  11791  expaddzlem  12353  expaddz  12354  expmulz  12356  ccatopth2  12881  swrdccat3  12902  resqrtcl  13394  limsupgle  13612  o1add  13754  o1mul  13755  o1sub  13756  bitsfzo  14488  sadfval  14505  smufval  14530  prmexpb  14749  4sqlem18OLD  14985  4sqlem18  14991  vdwlem10  15019  fsets  15227  submre  15589  mrelatlub  16510  mndodcong  17269  subgabl  17554  gex2abl  17567  cntzsubr  18118  abvres  18145  lbsind2  18382  lspsneu  18424  lbsextlem2  18460  lbsextg  18463  lindfind2  19453  matring  19545  maducoeval  19741  maducoeval2  19742  maduf  19743  madurid  19746  gsummatr01  19761  cramerimplem3  19787  cnprest  20382  hausnei2  20446  isreg2  20470  cmpcld  20494  llyrest  20577  nllyrest  20578  csdfil  20987  hausflimlem  21072  ssblps  21515  ssbl  21516  dvres2  22946  plyadd  23250  plymul  23251  coeeu  23258  vieta1  23344  aalioulem3  23369  aalioulem4  23370  efgh  23569  cxpadd  23703  cxpsub  23706  mulcxp  23709  divcxp  23711  cxple2  23721  cxplt2  23722  cxpcn3lem  23766  angcan  23810  ang180lem5  23821  isosctrlem3  23828  logexprlim  24232  abvcxp  24532  padicabv  24547  brbtwn2  25014  ax5seglem6  25043  axcontlem4  25076  axcontlem8  25080  clwwlknimp  25583  chscllem4  27374  ogrpinvlt  28561  poseq  30562  wsuclem  30579  nofulllem5  30666  ifscgr  30882  lshpnelb  32621  lfl1  32707  lshpkrlem6  32752  lshpkrex  32755  hlrelat3  33048  atbtwnexOLDN  33083  atbtwnex  33084  3dim3  33105  3atlem5  33123  2llnmat  33160  lvolex3N  33174  lvolnle3at  33218  4atlem11  33245  4atlem12  33248  dalemccea  33319  cdlema2N  33428  paddasslem2  33457  atmod1i1m  33494  lhp2lt  33637  lhp0lt  33639  lhpj1  33658  lhpmcvr4N  33662  lhpelim  33673  lhpmod2i2  33674  lhpmod6i1  33675  cdlemb2  33677  lhple  33678  lhpat  33679  4atex  33712  4atex2-0aOLDN  33714  4atex3  33717  ldilco  33752  ltrncl  33761  ltrn11  33762  ltrnle  33765  ltrncnvleN  33766  ltrnm  33767  ltrnj  33768  ltrncvr  33769  ltrnatb  33773  ltrnel  33775  ltrncnvel  33778  ltrncnv  33782  ltrnmwOLD  33788  trlval2  33800  trlcnv  33802  trljat1  33803  trljat2  33804  trl0  33807  ltrnnidn  33811  trlnidatb  33814  cdlemc1  33828  cdlemc2  33829  cdlemc5  33832  cdlemc6  33833  cdlemd3  33837  cdlemd6  33840  cdleme0aa  33847  cdleme0b  33849  cdleme0c  33850  cdleme0e  33854  cdleme0fN  33855  cdleme01N  33858  cdleme02N  33859  cdleme0ex1N  33860  cdleme0moN  33862  cdleme3g  33871  cdleme3h  33872  cdleme3  33874  cdleme4  33875  cdleme4a  33876  cdleme5  33877  cdleme8  33887  cdleme9  33890  cdleme10  33891  cdleme16aN  33896  cdleme11a  33897  cdleme11fN  33901  cdleme11g  33902  cdleme11h  33903  cdleme11j  33904  cdleme11k  33905  cdleme12  33908  cdleme13  33909  cdleme17c  33925  cdleme17d1  33926  cdleme18a  33928  cdleme18b  33929  cdleme18c  33930  cdleme22gb  33931  cdlemeda  33935  cdlemednpq  33936  cdlemednuN  33937  cdleme19c  33943  cdleme20aN  33947  cdleme20bN  33948  cdleme20c  33949  cdleme22aa  33977  cdleme22a  33978  cdleme22b  33979  cdleme22d  33981  cdleme22e  33982  cdleme27cl  34004  cdleme27a  34005  cdleme30a  34016  cdleme42a  34109  cdleme42c  34110  cdleme50laut  34185  cdlemf1  34199  cdlemf  34201  cdlemfnid  34202  trlord  34207  cdlemg2fv2  34238  cdlemg2kq  34240  cdlemg2m  34242  cdlemg4a  34246  cdlemg4d  34251  cdlemg4g  34254  cdlemg4  34255  cdlemg6c  34258  cdlemg7aN  34263  cdlemg8a  34265  cdlemg8b  34266  cdlemg8c  34267  cdlemg9a  34270  cdlemg9b  34271  cdlemg9  34272  cdlemg11aq  34276  cdlemg10c  34277  cdlemg12a  34281  cdlemg12b  34282  cdlemg12c  34283  cdlemg17a  34299  cdlemg18b  34317  cdlemg18c  34318  cdlemg31b0a  34333  cdlemg31a  34335  cdlemg31b  34336  cdlemg31d  34338  cdlemg35  34351  trlcoabs2N  34360  trlcolem  34364  cdlemg44a  34369  trljco  34378  trljco2  34379  tendoco2  34406  tendopltp  34418  cdlemi1  34456  cdlemi2  34457  cdlemj3  34461  tendocan  34462  cdlemk3  34471  cdlemk4  34472  cdlemk5a  34473  cdlemk9  34477  cdlemk9bN  34478  cdlemkvcl  34480  cdlemk10  34481  cdlemk30  34532  cdlemk31  34534  cdlemk39  34554  cdlemkfid1N  34559  cdlemkid1  34560  cdlemkid2  34562  cdlemkfid3N  34563  cdlemk19ylem  34568  cdlemk19xlem  34580  cdlemk19x  34581  cdlemk53b  34594  cdlemk53  34595  cdlemk54  34596  cdlemk55a  34597  cdlemk43N  34601  cdlemk19u1  34607  cdlemk19u  34608  cdleml1N  34614  erngdvlem4  34629  erngdvlem4-rN  34637  dia11N  34687  cdlemm10N  34757  dib11N  34799  cdlemn2  34834  cdlemn10  34845  dihjustlem  34855  dihord2cN  34860  dihlsscpre  34873  dih1dimb2  34880  dihvalcq2  34886  dihopelvalcpre  34887  dihord6b  34899  dih11  34904  dihmeetlem1N  34929  dihglblem2N  34933  dihglblem3N  34934  dihmeetlem2N  34938  dihglbcpreN  34939  dihmeetcN  34941  dihmeetbclemN  34943  dihmeetlem4preN  34945  dihmeetlem9N  34954  dihmeetlem20N  34965  dihlspsnssN  34971  dihlspsnat  34972  dihatlat  34973  dihglblem6  34979  dihmeet  34982  dochss  35004  hdmapval3N  35480  hgmap11  35544  congtr  35886  fzmaxdif  35902  isnumbasgrplem2  36034  ssmapsn  37569  infleinf  37682  mullimc  37793  mullimcf  37800  islpcn  37816  cncfuni  37861  icccncfext  37862  stoweidlem34  38007  stoweidlem59  38032  stirlinglem13  38060  fourierdlem41  38123  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem73  38155  sge0iunmptlemfi  38369  meadjiunlem  38419  ovncvrrp  38504  pfxccat3  39114  uhgr2edg  39453  nbgrisvtx  39591  nbupgrres  39602  lincscm  40731  lincext3  40757  el0ldep  40767  el0ldepsnzr  40768
  Copyright terms: Public domain W3C validator