Theorem simpll 518

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simp1ll  1044  simp2ll  1048  simp3ll  1052  rmob  2996  prneimg  3696  exmid01  4116  pwntru  4117  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  poinxp  4603  mpteqb  5504  fvmptt  5505  fcof1  5677  acexmid  5766  grprinvlem  5958  dftpos4  6153  tfrlem3ag  6199  tfrlem3a  6200  tfrlemi1  6222  tfrexlem  6224  tfr1onlem3ag  6227  nntr2  6392  dcdifsnid  6393  qsel  6499  ecopovsymg  6521  ecopoverg  6523  th3qlem1  6524  mapss  6578  xpmapenlem  6736  findcard2  6776  findcard2s  6777  findcard2sd  6779  unfiin  6807  f1finf1o  6828  fidcenumlemrk  6835  fidcenumlemr  6836  fidcenum  6837  sbthlemi6  6843  sbthlemi8  6845  elfi2  6853  supisolem  6888  enumct  6993  ismkvnex  7022  dfplpq2  7155  dfmpq2  7156  mulpipqqs  7174  distrnqg  7188  ltexnqq  7209  subhalfnqq  7215  prarloclemarch  7219  nnnq0lem1  7247  distrnq0  7260  npsspw  7272  prarloclemlo  7295  prarloclem3  7298  prarloclemcalc  7303  genplt2i  7311  distrlem1prl  7383  distrlem1pru  7384  distrlem4prl  7385  distrlem4pru  7386  ltprordil  7390  ltexprlemlol  7403  ltexprlemupu  7405  addextpr  7422  recexprlemopl  7426  recexprlemdisj  7431  recexprlem1ssl  7434  aptiprleml  7440  prsrlem1  7543  recexgt0sr  7574  addcnsr  7635  mulcnsr  7636  mulcnsrec  7644  axaddcl  7665  axmulcl  7667  axmulcom  7672  rereceu  7690  ltntri  7883  cnegexlem1  7930  cnegex  7933  addsub4  7998  le2add  8199  lt2add  8200  lt2sub  8215  le2sub  8216  rereim  8341  apreim  8358  mulreim  8359  addext  8365  mulext  8369  receuap  8423  rec11ap  8463  rec11rap  8464  divdivdivap  8466  ddcanap  8479  divadddivap  8480  divsubdivap  8481  conjmulap  8482  rerecclap  8483  subrecap  8591  recgt0  8601  prodgt0gt0  8602  prodgt0  8603  prodge0  8605  ltmul12a  8611  lemul12a  8613  lemulge11  8617  lt2mul2div  8630  ltrec  8634  lerec  8635  lt2msq  8637  ltrec1  8639  le2msq  8652  msq11  8653  ledivp1  8654  mulle0r  8695  peano5uzti  9152  eluzuzle  9327  qreccl  9427  xrltso  9575  z2ge  9602  xpncan  9647  xaddge0  9654  xle2add  9655  xleaddadd  9663  ixxss1  9680  ixxss2  9681  elioc2  9712  divelunit  9778  fzass4  9835  fzrev  9857  fzonmapblen  9957  elfzodifsumelfzo  9971  ssfzo12bi  9995  rebtwn2z  10025  qbtwnxr  10028  modqid  10115  modqcyc  10125  modqaddabs  10128  modqaddmod  10129  mulqaddmodid  10130  modqadd2mod  10140  modqltm1p1mod  10142  modqsubmod  10148  modqsubmodmod  10149  modqmulmod  10155  modqmulmodr  10156  modqsubdir  10159  frecuzrdgg  10182  seq3val  10224  seqvalcd  10225  seq3feq  10238  seq3f1olemp  10268  expp1  10293  expcl2lemap  10298  expnegzap  10320  expadd  10328  expmul  10331  leexp1a  10341  expnlbnd  10409  nn0opth2  10463  bcval  10488  bcval5  10502  bcpasc  10505  hashunsng  10546  seq3coll  10578  shftfvalg  10583  shftfval  10586  seq3shft  10603  caucvgrelemrec  10744  resqrexlemdecn  10777  sqrtmul  10800  sqrtdiv  10807  leabs  10839  absexpzap  10845  ltabs  10852  abslt  10853  absle  10854  abssubap0  10855  amgm2  10883  icodiamlt  10945  qdenre  10967  maxleim  10970  maxleastlt  10980  rexico  10986  zmaxcl  10989  minmax  10994  xrmaxleastlt  11018  xrminmax  11027  climuni  11055  cn1lem  11076  iserex  11101  iserle  11104  climserle  11107  climcau  11109  summodclem2a  11143  summodc  11145  isumss  11153  fisumss  11154  fsumadd  11168  isumadd  11193  fsum2dlemstep  11196  fsum2d  11197  fisum0diag2  11209  fsumabs  11227  isumsplit  11253  geolim  11273  geo2lim  11278  geoisum  11279  geoisumr  11280  geoisum1  11281  mertenslemub  11296  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  efcvgfsum  11362  eftlcl  11383  reeftlcl  11384  tanaddap  11435  zdvdsdc  11503  dvds2ln  11515  dvdsle  11531  divconjdvds  11536  dvdsext  11542  gcdsupex  11635  gcdsupcl  11636  bezoutlemmain  11675  bezoutlemaz  11680  bezoutlembi  11682  bezout  11688  gcdmultiplez  11698  dvdsmulgcd  11702  bezoutr  11709  bezoutr1  11710  lcmval  11733  lcmcllem  11737  ncoprmgcdne1b  11759  cncongr1  11773  prmdvdsexp  11815  sqrt2irr  11829  pw2dvdslemn  11832  pw2dvdseu  11835  nonsq  11874  isstruct2r  11959  setsfun  11983  setsfun0  11984  neissex  12323  tgrest  12327  ssrest  12340  restopn2  12341  cnco  12379  cnss1  12384  cnss2  12385  cnptopresti  12396  uptx  12432  txrest  12434  psmetres2  12491  xmetres2  12537  xblss2ps  12562  blhalf  12566  blssexps  12587  blssex  12588  blin2  12590  blbas  12591  bdmetval  12658  metcnpi  12673  metcnpi2  12674  qtopbas  12680  tgqioo  12705  cncfss  12728  mulc1cncf  12734  cncfmptid  12741  dedekindicc  12769  ivthdec  12780  cnplimcim  12794  cnplimclemle  12795  cnplimccntop  12797  limccnp2cntop  12804  dvfgg  12815  dvcj  12831  dvrecap  12835  dveflem  12844  ptolemy  12894  pwtrufal  13181  nninfalllem1  13192  nninfsellemqall  13200  sbthom  13210  qdencn  13211  isomninnlem  13214