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  4648  funprg  5267  omeulem2  6577  unxpdomlem3  7065  elfiun  7179  cantnffval  7360  tcrank  7550  cofsmo  7891  isfin2-2  7941  tskint  8403  tskun  8404  tskurn  8407  gruina  8436  dmdcan  9466  lt2msq1  9635  supmullem1  9716  supmul  9718  xaddass  10565  xaddass2  10566  xlt2add  10576  xmulasslem3  10602  xadddi2r  10614  iccsplit  10764  expaddzlem  11141  expaddz  11142  expmulz  11144  ccatopth2  11459  resqrcl  11735  limsupgle  11947  o1add  12083  o1mul  12084  o1sub  12085  bitsfzo  12622  sadfval  12639  smufval  12664  prmexpb  12792  4sqlem18  13005  vdwlem10  13033  submre  13503  mrelatlub  14285  spwpr4  14336  mndodcong  14853  subgabl  15128  gex2abl  15139  cntzsubr  15573  abvres  15600  lbsind2  15830  lspsneu  15872  lbsextlem2  15908  lbsextg  15911  cnprest  17013  hausnei2  17077  isreg2  17101  cmpcld  17125  llyrest  17207  nllyrest  17208  csdfil  17585  hausflimlem  17670  ssbl  17967  dvres2  19258  plyadd  19595  plymul  19596  coeeu  19603  vieta1  19688  aalioulem3  19710  aalioulem4  19711  cxpadd  20022  cxpsub  20025  mulcxp  20028  divcxp  20030  cxple2  20040  cxplt2  20041  cxpcn3lem  20083  angcan  20096  ang180lem5  20107  isosctrlem3  20116  logexprlim  20460  abvcxp  20760  padicabv  20775  chscllem4  22215  dedekind  23488  poseq  23657  brbtwn2  23943  ax5seglem6  23972  axcontlem4  24005  axcontlem8  24009  ifscgr  24077  uninqs  24449  intopcoaconlem3b  24949  prdnei  24984  islimrs  24991  flfneic  25035  setiscat  25390  congtr  26463  fzmaxdif  26479  isnumbasgrplem2  26680  lindfind2  26699  matrng  26891  refsumcn  27112  fmuldfeq  27124  stoweidlem31  27191  stoweidlem34  27194  stoweidlem43  27203  stoweidlem46  27206  stoweidlem52  27212  stoweidlem53  27213  stoweidlem54  27214  stoweidlem55  27215  stoweidlem56  27216  stoweidlem57  27217  stoweidlem58  27218  stoweidlem59  27219  stoweidlem60  27220  stoweid  27223  stirlinglem13  27246  lshpnelb  28453  lfl1  28539  lshpkrlem6  28584  lshpkrex  28587  hlrelat3  28880  atbtwnexOLDN  28915  atbtwnex  28916  3dim3  28937  3atlem5  28955  2llnmat  28992  lvolex3N  29006  lvolnle3at  29050  4atlem11  29077  4atlem12  29080  dalemccea  29151  cdlema2N  29260  paddasslem2  29289  atmod1i1m  29326  lhp2lt  29469  lhp0lt  29471  lhpj1  29490  lhpmcvr4N  29494  lhpelim  29505  lhpmod2i2  29506  lhpmod6i1  29507  cdlemb2  29509  lhple  29510  lhpat  29511  4atex  29544  4atex2-0aOLDN  29546  4atex3  29549  ldilco  29584  ltrncl  29593  ltrn11  29594  ltrnle  29597  ltrncnvleN  29598  ltrnm  29599  ltrnj  29600  ltrncvr  29601  ltrnatb  29605  ltrnel  29607  ltrncnvel  29610  ltrncnv  29614  ltrnmw  29619  trlval2  29631  trlcnv  29633  trljat1  29634  trljat2  29635  trl0  29638  ltrnnidn  29642  trlnidatb  29645  cdlemc1  29659  cdlemc2  29660  cdlemc5  29663  cdlemc6  29664  cdlemd3  29668  cdlemd6  29671  cdleme0aa  29678  cdleme0b  29680  cdleme0c  29681  cdleme0e  29685  cdleme0fN  29686  cdleme01N  29689  cdleme02N  29690  cdleme0ex1N  29691  cdleme0moN  29693  cdleme3g  29702  cdleme3h  29703  cdleme3  29705  cdleme4  29706  cdleme4a  29707  cdleme5  29708  cdleme8  29718  cdleme9  29721  cdleme10  29722  cdleme16aN  29727  cdleme11a  29728  cdleme11fN  29732  cdleme11g  29733  cdleme11h  29734  cdleme11j  29735  cdleme11k  29736  cdleme12  29739  cdleme13  29740  cdleme17c  29756  cdleme17d1  29757  cdleme18a  29759  cdleme18b  29760  cdleme18c  29761  cdleme22gb  29762  cdlemeda  29766  cdlemednpq  29767  cdlemednuN  29768  cdleme19c  29773  cdleme20aN  29777  cdleme20bN  29778  cdleme20c  29779  cdleme22aa  29807  cdleme22a  29808  cdleme22b  29809  cdleme22d  29811  cdleme22e  29812  cdleme27cl  29834  cdleme27a  29835  cdleme30a  29846  cdleme42a  29939  cdleme42c  29940  cdleme50laut  30015  cdlemf1  30029  cdlemf  30031  cdlemfnid  30032  trlord  30037  cdlemg2fv2  30068  cdlemg2kq  30070  cdlemg2m  30072  cdlemg4a  30076  cdlemg4d  30081  cdlemg4g  30084  cdlemg4  30085  cdlemg6c  30088  cdlemg7aN  30093  cdlemg8a  30095  cdlemg8b  30096  cdlemg8c  30097  cdlemg9a  30100  cdlemg9b  30101  cdlemg9  30102  cdlemg11aq  30106  cdlemg10c  30107  cdlemg12a  30111  cdlemg12b  30112  cdlemg12c  30113  cdlemg17a  30129  cdlemg18b  30147  cdlemg18c  30148  cdlemg31b0a  30163  cdlemg31a  30165  cdlemg31b  30166  cdlemg31d  30168  cdlemg35  30181  trlcoabs2N  30190  trlcolem  30194  cdlemg44a  30199  trljco  30208  trljco2  30209  tendoco2  30236  tendopltp  30248  cdlemi1  30286  cdlemi2  30287  cdlemj3  30291  tendocan  30292  cdlemk3  30301  cdlemk4  30302  cdlemk5a  30303  cdlemk9  30307  cdlemk9bN  30308  cdlemkvcl  30310  cdlemk10  30311  cdlemk30  30362  cdlemk31  30364  cdlemk39  30384  cdlemkfid1N  30389  cdlemkid1  30390  cdlemkid2  30392  cdlemkfid3N  30393  cdlemk19ylem  30398  cdlemk19xlem  30410  cdlemk19x  30411  cdlemk53b  30424  cdlemk53  30425  cdlemk54  30426  cdlemk55a  30427  cdlemk43N  30431  cdlemk19u1  30437  cdlemk19u  30438  cdleml1N  30444  erngdvlem4  30459  erngdvlem4-rN  30467  dia11N  30517  cdlemm10N  30587  dib11N  30629  cdlemn2  30664  cdlemn10  30675  dihjustlem  30685  dihord2cN  30690  dihlsscpre  30703  dih1dimb2  30710  dihvalcq2  30716  dihopelvalcpre  30717  dihord6b  30729  dih11  30734  dihmeetlem1N  30759  dihglblem2N  30763  dihglblem3N  30764  dihmeetlem2N  30768  dihglbcpreN  30769  dihmeetcN  30771  dihmeetbclemN  30773  dihmeetlem4preN  30775  dihmeetlem9N  30784  dihmeetlem20N  30795  dihlspsnssN  30801  dihlspsnat  30802  dihatlat  30803  dihglblem6  30809  dochss  30834  hdmapval3N  31310  hgmap11  31374
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