Theorem simpll 501

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 477	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simp1ll  1027  simp2ll  1031  simp3ll  1035  rmob  2969  prneimg  3667  exmid01  4081  pwntru  4082  ordtri2or2exmidlem  4401  onsucelsucexmidlem  4404  poinxp  4568  mpteqb  5465  fvmptt  5466  fcof1  5638  acexmid  5727  grprinvlem  5919  dftpos4  6114  tfrlem3ag  6160  tfrlem3a  6161  tfrlemi1  6183  tfrexlem  6185  tfr1onlem3ag  6188  nntr2  6353  dcdifsnid  6354  qsel  6460  ecopovsymg  6482  ecopoverg  6484  th3qlem1  6485  mapss  6539  xpmapenlem  6696  findcard2  6736  findcard2s  6737  findcard2sd  6739  unfiin  6767  f1finf1o  6787  fidcenumlemrk  6794  fidcenumlemr  6795  fidcenum  6796  sbthlemi6  6802  sbthlemi8  6804  elfi2  6812  supisolem  6847  enumct  6952  ismkvnex  6979  dfplpq2  7110  dfmpq2  7111  mulpipqqs  7129  distrnqg  7143  ltexnqq  7164  subhalfnqq  7170  prarloclemarch  7174  nnnq0lem1  7202  distrnq0  7215  npsspw  7227  prarloclemlo  7250  prarloclem3  7253  prarloclemcalc  7258  genplt2i  7266  distrlem1prl  7338  distrlem1pru  7339  distrlem4prl  7340  distrlem4pru  7341  ltprordil  7345  ltexprlemlol  7358  ltexprlemupu  7360  addextpr  7377  recexprlemopl  7381  recexprlemdisj  7386  recexprlem1ssl  7389  aptiprleml  7395  prsrlem1  7485  recexgt0sr  7516  addcnsr  7569  mulcnsr  7570  mulcnsrec  7578  axaddcl  7599  axmulcl  7601  axmulcom  7606  rereceu  7624  ltntri  7813  cnegexlem1  7860  cnegex  7863  addsub4  7928  le2add  8125  lt2add  8126  lt2sub  8141  le2sub  8142  rereim  8266  apreim  8283  mulreim  8284  addext  8290  mulext  8294  receuap  8343  rec11ap  8383  rec11rap  8384  divdivdivap  8386  ddcanap  8399  divadddivap  8400  divsubdivap  8401  conjmulap  8402  rerecclap  8403  recgt0  8518  prodgt0gt0  8519  prodgt0  8520  prodge0  8522  ltmul12a  8528  lemul12a  8530  lemulge11  8534  lt2mul2div  8547  ltrec  8551  lerec  8552  lt2msq  8554  ltrec1  8556  le2msq  8569  msq11  8570  ledivp1  8571  mulle0r  8612  peano5uzti  9063  eluzuzle  9236  qreccl  9336  xrltso  9475  z2ge  9502  xpncan  9547  xaddge0  9554  xle2add  9555  xleaddadd  9563  ixxss1  9580  ixxss2  9581  elioc2  9612  divelunit  9678  fzass4  9735  fzrev  9757  fzonmapblen  9857  elfzodifsumelfzo  9871  ssfzo12bi  9895  rebtwn2z  9925  qbtwnxr  9928  modqid  10015  modqcyc  10025  modqaddabs  10028  modqaddmod  10029  mulqaddmodid  10030  modqadd2mod  10040  modqltm1p1mod  10042  modqsubmod  10048  modqsubmodmod  10049  modqmulmod  10055  modqmulmodr  10056  modqsubdir  10059  frecuzrdgg  10082  seq3val  10124  seqvalcd  10125  seq3feq  10138  seq3f1olemp  10168  expp1  10193  expcl2lemap  10198  expnegzap  10220  expadd  10228  expmul  10231  leexp1a  10241  expnlbnd  10309  nn0opth2  10363  bcval  10388  bcval5  10402  bcpasc  10405  hashunsng  10446  seq3coll  10478  shftfvalg  10483  shftfval  10486  seq3shft  10503  caucvgrelemrec  10643  resqrexlemdecn  10676  sqrtmul  10699  sqrtdiv  10706  leabs  10738  absexpzap  10744  ltabs  10751  abslt  10752  absle  10753  abssubap0  10754  amgm2  10782  icodiamlt  10844  qdenre  10866  maxleim  10869  maxleastlt  10879  rexico  10885  zmaxcl  10888  minmax  10893  xrmaxleastlt  10917  xrminmax  10926  climuni  10954  cn1lem  10975  iserex  11000  iserle  11003  climserle  11006  climcau  11008  summodclem2a  11042  summodc  11044  isumss  11052  fisumss  11053  fsumadd  11067  isumadd  11092  fsum2dlemstep  11095  fsum2d  11096  fisum0diag2  11108  fsumabs  11126  isumsplit  11152  geolim  11172  geo2lim  11177  geoisum  11178  geoisumr  11179  geoisum1  11180  mertenslemub  11195  mertenslemi1  11196  mertenslem2  11197  mertensabs  11198  efcvgfsum  11224  eftlcl  11245  reeftlcl  11246  tanaddap  11297  zdvdsdc  11362  dvds2ln  11374  dvdsle  11390  divconjdvds  11395  dvdsext  11401  gcdsupex  11494  gcdsupcl  11495  bezoutlemmain  11532  bezoutlemaz  11537  bezoutlembi  11539  bezout  11545  gcdmultiplez  11555  dvdsmulgcd  11559  bezoutr  11566  bezoutr1  11567  lcmval  11590  lcmcllem  11594  ncoprmgcdne1b  11616  cncongr1  11630  prmdvdsexp  11672  sqrt2irr  11686  pw2dvdslemn  11688  pw2dvdseu  11691  nonsq  11730  isstruct2r  11813  setsfun  11837  setsfun0  11838  neissex  12177  tgrest  12181  ssrest  12194  restopn2  12195  cnco  12232  cnss1  12237  cnss2  12238  cnptopresti  12249  uptx  12285  txrest  12287  psmetres2  12322  xmetres2  12368  xblss2ps  12393  blhalf  12397  blssexps  12418  blssex  12419  blin2  12421  blbas  12422  bdmetval  12489  metcnpi  12504  metcnpi2  12505  qtopbas  12511  tgqioo  12533  cncfss  12556  mulc1cncf  12562  cncfmptid  12569  cnplimcim  12592  cnplimclemle  12593  cnplimccntop  12595  limccnp2cntop  12602  dvfgg  12612  pwtrufal  12884  nninfalllem1  12895  nninfsellemqall  12903  sbthom  12913  qdencn  12914  isomninnlem  12917