Theorem simpll 527

Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)

Assertion

Ref	Expression
simpll	|- ( ( ( ph /\ ps ) /\ ch ) -> ph )

Proof of Theorem simpll

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2	1	ad2antrr 488	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp1ll  1062  simp2ll  1066  simp3ll  1070  rmob  3090  ifnefals  3613  prneimg  3814  exmid01  4241  pwntru  4242  ordtri2or2exmidlem  4573  onsucelsucexmidlem  4576  poinxp  4743  mpteqb  5669  fvmptt  5670  fcof1  5851  acexmid  5942  dftpos4  6348  tfrlem3ag  6394  tfrlem3a  6395  tfrlemi1  6417  tfrexlem  6419  tfr1onlem3ag  6422  nntr2  6588  dcdifsnid  6589  qsel  6698  ecopovsymg  6720  ecopoverg  6722  th3qlem1  6723  mapss  6777  xpmapenlem  6945  findcard2  6985  findcard2s  6986  findcard2sd  6988  unfiin  7022  f1finf1o  7048  fidcenumlemrk  7055  fidcenumlemr  7056  fidcenum  7057  sbthlemi6  7063  sbthlemi8  7065  elfi2  7073  supisolem  7109  enumct  7216  nninfninc  7224  ismkvnex  7256  exmidontriimlem4  7335  netap  7365  2omotaplemap  7368  cc2lem  7377  dfplpq2  7466  dfmpq2  7467  mulpipqqs  7485  distrnqg  7499  ltexnqq  7520  subhalfnqq  7526  prarloclemarch  7530  nnnq0lem1  7558  distrnq0  7571  npsspw  7583  prarloclemlo  7606  prarloclem3  7609  prarloclemcalc  7614  genplt2i  7622  distrlem1prl  7694  distrlem1pru  7695  distrlem4prl  7696  distrlem4pru  7697  ltprordil  7701  ltexprlemlol  7714  ltexprlemupu  7716  addextpr  7733  recexprlemopl  7737  recexprlemdisj  7742  recexprlem1ssl  7745  aptiprleml  7751  prsrlem1  7854  recexgt0sr  7885  addcnsr  7946  mulcnsr  7947  mulcnsrec  7955  axaddcl  7976  axmulcl  7978  axmulcom  7983  rereceu  8001  mpomulf  8061  ltntri  8199  cnegexlem1  8246  cnegex  8249  addsub4  8314  le2add  8516  lt2add  8517  lt2sub  8532  le2sub  8533  rereim  8658  apreim  8675  mulreim  8676  addext  8682  mulext  8686  receuap  8741  rec11ap  8782  rec11rap  8783  divdivdivap  8785  ddcanap  8798  divadddivap  8799  divsubdivap  8800  conjmulap  8801  rerecclap  8802  subrecap  8911  recgt0  8922  prodgt0gt0  8923  prodgt0  8924  prodge0  8926  ltmul12a  8932  lemul12a  8934  lemulge11  8938  lt2mul2div  8951  ltrec  8955  lerec  8956  lt2msq  8958  ltrec1  8960  le2msq  8973  msq11  8974  ledivp1  8975  mulle0r  9016  peano5uzti  9480  eluzuzle  9655  qreccl  9762  elpq  9769  xrltso  9917  z2ge  9947  xpncan  9992  xaddge0  9999  xle2add  10000  xleaddadd  10008  ixxss1  10025  ixxss2  10026  elioc2  10057  divelunit  10123  fzass4  10183  fzrev  10205  fzonmapblen  10309  elfzodifsumelfzo  10328  ssfzo12bi  10352  rebtwn2z  10395  qbtwnxr  10398  modqid  10492  modqcyc  10502  modqaddabs  10505  modqaddmod  10506  mulqaddmodid  10507  modqadd2mod  10517  modqltm1p1mod  10519  modqsubmod  10525  modqsubmodmod  10526  modqmulmod  10532  modqmulmodr  10533  modqsubdir  10536  frecuzrdgg  10559  nninfinf  10586  seq3val  10603  seqvalcd  10604  seq3feq  10623  seq3f1olemp  10658  seqfeq4g  10674  expp1  10689  expcl2lemap  10694  expnegzap  10716  expadd  10724  expmul  10727  leexp1a  10737  expnlbnd  10807  nn0ltexp2  10852  nn0opth2  10867  bcval  10892  bcval5  10906  bcpasc  10909  hashunsng  10950  seq3coll  10985  iswrdiz  10999  sswrd  11001  shftfvalg  11071  shftfval  11074  seq3shft  11091  caucvgrelemrec  11232  resqrexlemdecn  11265  sqrtmul  11288  sqrtdiv  11295  leabs  11327  absexpzap  11333  ltabs  11340  abslt  11341  absle  11342  abssubap0  11343  amgm2  11371  icodiamlt  11433  qdenre  11455  maxleim  11458  maxleastlt  11468  rexico  11474  zmaxcl  11477  minmax  11483  xrmaxleastlt  11509  xrminmax  11518  climuni  11546  cn1lem  11567  iserex  11592  iserle  11595  climserle  11598  climcau  11600  summodclem2a  11634  summodc  11636  isumss  11644  fisumss  11645  fsumadd  11659  isumadd  11684  fsum2dlemstep  11687  fsum2d  11688  fisum0diag2  11700  fsumabs  11718  isumsplit  11744  geolim  11764  geo2lim  11769  geoisum  11770  geoisumr  11771  geoisum1  11772  mertenslemub  11787  mertenslemi1  11788  mertenslem2  11789  mertensabs  11790  prodmodclem2  11830  prodmodc  11831  zproddc  11832  fprodseq  11836  fprodcl2lem  11858  fprod2dlemstep  11875  fprodle  11893  fprodmodd  11894  efcvgfsum  11920  eftlcl  11941  reeftlcl  11942  tanaddap  11992  zdvdsdc  12065  dvds2ln  12077  dvdsle  12097  divconjdvds  12102  dvdsext  12108  bitsfzo  12208  gcdsupex  12220  gcdsupcl  12221  bezoutlemmain  12261  bezoutlemaz  12266  bezoutlembi  12268  bezout  12274  gcdmultiplez  12284  dvdsmulgcd  12288  bezoutr  12295  bezoutr1  12296  lcmval  12327  lcmcllem  12331  ncoprmgcdne1b  12353  cncongr1  12367  isprm5  12406  prmdvdsexp  12412  sqrt2irr  12426  pw2dvdslemn  12429  pw2dvdseu  12432  nonsq  12471  powm2modprm  12517  pcmul  12566  pcqmul  12568  pcexp  12574  pcneg  12590  pcdvdstr  12592  pcprmpw2  12598  pcfac  12615  expnprm  12618  prmpwdvds  12620  mul4sq  12659  ssnnctlemct  12759  infpn2  12769  isstruct2r  12785  setsfun  12809  setsfun0  12810  ismndd  13211  submnd0  13218  mhmf1o  13244  resmhm  13261  mhmco  13264  mhmima  13265  dfgrp2  13301  grprcan  13311  grplmulf1o  13348  grplactcnv  13376  pwssub  13387  mhmmnd  13394  mulgval  13400  mulgz  13428  mulgnn0dir  13430  mulgdir  13432  mulgneg2  13434  mhmmulg  13441  issubg4m  13471  nmzsubg  13488  ssnmz  13489  ghmmhmb  13532  resghm  13538  ghmpreima  13544  ghmnsgpreima  13547  ghmf1o  13553  eqgabl  13608  gsumfzconst  13619  rngpropd  13659  srglmhm  13697  srgrmhm  13698  isring  13704  ringadd2  13731  ringpropd  13742  ringlghm  13765  ringrghm  13766  oppr1g  13786  dvdsrex  13802  dvdsrtr  13805  issubrg  13925  unitrrg  13971  islmod  13995  islmodd  13997  lmodfopne  14030  lmodprop2d  14052  lssvacl  14069  lssvsubcl  14070  lssvscl  14079  islss3  14083  lsslss  14085  lss1d  14087  lsspropdg  14135  dflidl2rng  14185  gsumfzfsumlemm  14291  expghmap  14311  mulgghm2  14312  znval  14340  znunit  14363  znrrg  14364  psrbaglesuppg  14376  mplvalcoe  14394  neissex  14579  tgrest  14583  ssrest  14596  restopn2  14597  cnco  14635  cnss1  14640  cnss2  14641  cnptopresti  14652  uptx  14688  txrest  14690  psmetres2  14747  xmetres2  14793  xblss2ps  14818  blhalf  14822  blssexps  14843  blssex  14844  blin2  14846  blbas  14847  bdmetval  14914  metcnpi  14929  metcnpi2  14930  qtopbas  14936  tgqioo  14969  cncfss  14997  mulc1cncf  15003  cncfmptid  15011  dedekindicc  15047  ivthdec  15058  cnplimcim  15081  cnplimclemle  15082  cnplimccntop  15084  limccnp2cntop  15091  dvfgg  15102  dvcj  15123  dvrecap  15127  dvmptfsum  15139  dveflem  15140  elply2  15149  ply1termlem  15156  plymullem1  15162  eflt  15189  ptolemy  15238  cos11  15267  rpcxpmul2  15327  cxplt  15330  cxple  15331  cxplt3  15334  apcxp2  15353  rprelogbmul  15369  rprelogbdiv  15371  sgmval  15397  sgmval2  15398  sgmf  15400  sgmmul  15410  perfect  15415  lgsval2lem  15429  lgsdir2lem5  15451  2sqlem6  15539  2omap  15865  pwtrufal  15867  nninfalllem1  15878  nninfsellemqall  15885  nnnninfex  15892  sbthom  15898  qdencn  15899  isomninnlem  15902  trirec0  15916  apdiff  15920  iswomninnlem  15921  ismkvnnlem  15924  ltlenmkv  15942