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

Theorem simp1l 1007
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 454 . 2  |-  ( (
ph  /\  ps )  ->  ph )
213ad2ant1 1004 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 185  df-an 371  df-3an 962
This theorem is referenced by:  simpl1l  1034  simpr1l  1040  simp11l  1094  simp21l  1100  simp31l  1106  funprg  5464  tfisi  6468  omeulem2  7018  uniinqs  7176  unxpdomlem3  7515  elfiun  7676  cantnffval  7865  tcrank  8087  cofsmo  8434  isfin2-2  8484  tskint  8948  tskun  8949  tskurn  8952  gruina  8981  dedekind  9529  dmdcan  10037  lt2msq1  10211  supmullem1  10292  supmul  10294  xaddass  11208  xaddass2  11209  xlt2add  11219  xmulasslem3  11245  xadddi2r  11257  iccsplit  11414  expaddzlem  11903  expaddz  11904  expmulz  11906  ccatopth2  12361  swrdccat3  12379  resqrcl  12739  limsupgle  12951  o1add  13087  o1mul  13088  o1sub  13089  bitsfzo  13627  sadfval  13644  smufval  13669  prmexpb  13799  4sqlem18  14019  vdwlem10  14047  fsets  14196  submre  14539  mrelatlub  15352  mndodcong  16038  subgabl  16313  gex2abl  16326  cntzsubr  16877  abvres  16904  lbsind2  17140  lspsneu  17182  lbsextlem2  17218  lbsextg  17221  lindfind2  18206  matrng  18289  maducoeval  18404  maducoeval2  18405  maduf  18406  madurid  18409  gsummatr01  18424  cramerimplem3  18450  cnprest  18852  hausnei2  18916  isreg2  18940  cmpcld  18964  llyrest  19048  nllyrest  19049  csdfil  19426  hausflimlem  19511  ssblps  19956  ssbl  19957  dvres2  21346  plyadd  21644  plymul  21645  coeeu  21652  vieta1  21737  aalioulem3  21759  aalioulem4  21760  cxpadd  22083  cxpsub  22086  mulcxp  22089  divcxp  22091  cxple2  22101  cxplt2  22102  cxpcn3lem  22144  angcan  22157  ang180lem5  22168  isosctrlem3  22177  logexprlim  22523  abvcxp  22823  padicabv  22838  brbtwn2  23086  ax5seglem6  23115  axcontlem4  23148  axcontlem8  23152  chscllem4  24978  ogrpinvlt  26120  poseq  27643  wsuclem  27691  nofulllem5  27776  ifscgr  28004  congtr  29233  fzmaxdif  29249  isnumbasgrplem2  29385  stoweidlem34  29754  stoweidlem59  29779  stirlinglem13  29806  clwwlknimp  30364  lincscm  30805  lincext3  30831  el0ldep  30841  el0ldepsnzr  30842  lshpnelb  32351  lfl1  32437  lshpkrlem6  32482  lshpkrex  32485  hlrelat3  32778  atbtwnexOLDN  32813  atbtwnex  32814  3dim3  32835  3atlem5  32853  2llnmat  32890  lvolex3N  32904  lvolnle3at  32948  4atlem11  32975  4atlem12  32978  dalemccea  33049  cdlema2N  33158  paddasslem2  33187  atmod1i1m  33224  lhp2lt  33367  lhp0lt  33369  lhpj1  33388  lhpmcvr4N  33392  lhpelim  33403  lhpmod2i2  33404  lhpmod6i1  33405  cdlemb2  33407  lhple  33408  lhpat  33409  4atex  33442  4atex2-0aOLDN  33444  4atex3  33447  ldilco  33482  ltrncl  33491  ltrn11  33492  ltrnle  33495  ltrncnvleN  33496  ltrnm  33497  ltrnj  33498  ltrncvr  33499  ltrnatb  33503  ltrnel  33505  ltrncnvel  33508  ltrncnv  33512  ltrnmw  33517  trlval2  33529  trlcnv  33531  trljat1  33532  trljat2  33533  trl0  33536  ltrnnidn  33540  trlnidatb  33543  cdlemc1  33557  cdlemc2  33558  cdlemc5  33561  cdlemc6  33562  cdlemd3  33566  cdlemd6  33569  cdleme0aa  33576  cdleme0b  33578  cdleme0c  33579  cdleme0e  33583  cdleme0fN  33584  cdleme01N  33587  cdleme02N  33588  cdleme0ex1N  33589  cdleme0moN  33591  cdleme3g  33600  cdleme3h  33601  cdleme3  33603  cdleme4  33604  cdleme4a  33605  cdleme5  33606  cdleme8  33616  cdleme9  33619  cdleme10  33620  cdleme16aN  33625  cdleme11a  33626  cdleme11fN  33630  cdleme11g  33631  cdleme11h  33632  cdleme11j  33633  cdleme11k  33634  cdleme12  33637  cdleme13  33638  cdleme17c  33654  cdleme17d1  33655  cdleme18a  33657  cdleme18b  33658  cdleme18c  33659  cdleme22gb  33660  cdlemeda  33664  cdlemednpq  33665  cdlemednuN  33666  cdleme19c  33671  cdleme20aN  33675  cdleme20bN  33676  cdleme20c  33677  cdleme22aa  33705  cdleme22a  33706  cdleme22b  33707  cdleme22d  33709  cdleme22e  33710  cdleme27cl  33732  cdleme27a  33733  cdleme30a  33744  cdleme42a  33837  cdleme42c  33838  cdleme50laut  33913  cdlemf1  33927  cdlemf  33929  cdlemfnid  33930  trlord  33935  cdlemg2fv2  33966  cdlemg2kq  33968  cdlemg2m  33970  cdlemg4a  33974  cdlemg4d  33979  cdlemg4g  33982  cdlemg4  33983  cdlemg6c  33986  cdlemg7aN  33991  cdlemg8a  33993  cdlemg8b  33994  cdlemg8c  33995  cdlemg9a  33998  cdlemg9b  33999  cdlemg9  34000  cdlemg11aq  34004  cdlemg10c  34005  cdlemg12a  34009  cdlemg12b  34010  cdlemg12c  34011  cdlemg17a  34027  cdlemg18b  34045  cdlemg18c  34046  cdlemg31b0a  34061  cdlemg31a  34063  cdlemg31b  34064  cdlemg31d  34066  cdlemg35  34079  trlcoabs2N  34088  trlcolem  34092  cdlemg44a  34097  trljco  34106  trljco2  34107  tendoco2  34134  tendopltp  34146  cdlemi1  34184  cdlemi2  34185  cdlemj3  34189  tendocan  34190  cdlemk3  34199  cdlemk4  34200  cdlemk5a  34201  cdlemk9  34205  cdlemk9bN  34206  cdlemkvcl  34208  cdlemk10  34209  cdlemk30  34260  cdlemk31  34262  cdlemk39  34282  cdlemkfid1N  34287  cdlemkid1  34288  cdlemkid2  34290  cdlemkfid3N  34291  cdlemk19ylem  34296  cdlemk19xlem  34308  cdlemk19x  34309  cdlemk53b  34322  cdlemk53  34323  cdlemk54  34324  cdlemk55a  34325  cdlemk43N  34329  cdlemk19u1  34335  cdlemk19u  34336  cdleml1N  34342  erngdvlem4  34357  erngdvlem4-rN  34365  dia11N  34415  cdlemm10N  34485  dib11N  34527  cdlemn2  34562  cdlemn10  34573  dihjustlem  34583  dihord2cN  34588  dihlsscpre  34601  dih1dimb2  34608  dihvalcq2  34614  dihopelvalcpre  34615  dihord6b  34627  dih11  34632  dihmeetlem1N  34657  dihglblem2N  34661  dihglblem3N  34662  dihmeetlem2N  34666  dihglbcpreN  34667  dihmeetcN  34669  dihmeetbclemN  34671  dihmeetlem4preN  34673  dihmeetlem9N  34682  dihmeetlem20N  34693  dihlspsnssN  34699  dihlspsnat  34700  dihatlat  34701  dihglblem6  34707  dihmeet  34710  dochss  34732  hdmapval3N  35208  hgmap11  35272
  Copyright terms: Public domain W3C validator