Theorem simpll 519

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 480	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  1050  simp2ll  1054  simp3ll  1058  rmob  3043  prneimg  3754  exmid01  4177  pwntru  4178  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  poinxp  4673  mpteqb  5576  fvmptt  5577  fcof1  5751  acexmid  5841  dftpos4  6231  tfrlem3ag  6277  tfrlem3a  6278  tfrlemi1  6300  tfrexlem  6302  tfr1onlem3ag  6305  nntr2  6471  dcdifsnid  6472  qsel  6578  ecopovsymg  6600  ecopoverg  6602  th3qlem1  6603  mapss  6657  xpmapenlem  6815  findcard2  6855  findcard2s  6856  findcard2sd  6858  unfiin  6891  f1finf1o  6912  fidcenumlemrk  6919  fidcenumlemr  6920  fidcenum  6921  sbthlemi6  6927  sbthlemi8  6929  elfi2  6937  supisolem  6973  enumct  7080  ismkvnex  7119  exmidontriimlem4  7180  cc2lem  7207  dfplpq2  7295  dfmpq2  7296  mulpipqqs  7314  distrnqg  7328  ltexnqq  7349  subhalfnqq  7355  prarloclemarch  7359  nnnq0lem1  7387  distrnq0  7400  npsspw  7412  prarloclemlo  7435  prarloclem3  7438  prarloclemcalc  7443  genplt2i  7451  distrlem1prl  7523  distrlem1pru  7524  distrlem4prl  7525  distrlem4pru  7526  ltprordil  7530  ltexprlemlol  7543  ltexprlemupu  7545  addextpr  7562  recexprlemopl  7566  recexprlemdisj  7571  recexprlem1ssl  7574  aptiprleml  7580  prsrlem1  7683  recexgt0sr  7714  addcnsr  7775  mulcnsr  7776  mulcnsrec  7784  axaddcl  7805  axmulcl  7807  axmulcom  7812  rereceu  7830  ltntri  8026  cnegexlem1  8073  cnegex  8076  addsub4  8141  le2add  8342  lt2add  8343  lt2sub  8358  le2sub  8359  rereim  8484  apreim  8501  mulreim  8502  addext  8508  mulext  8512  receuap  8566  rec11ap  8606  rec11rap  8607  divdivdivap  8609  ddcanap  8622  divadddivap  8623  divsubdivap  8624  conjmulap  8625  rerecclap  8626  subrecap  8735  recgt0  8745  prodgt0gt0  8746  prodgt0  8747  prodge0  8749  ltmul12a  8755  lemul12a  8757  lemulge11  8761  lt2mul2div  8774  ltrec  8778  lerec  8779  lt2msq  8781  ltrec1  8783  le2msq  8796  msq11  8797  ledivp1  8798  mulle0r  8839  peano5uzti  9299  eluzuzle  9474  qreccl  9580  elpq  9586  xrltso  9732  z2ge  9762  xpncan  9807  xaddge0  9814  xle2add  9815  xleaddadd  9823  ixxss1  9840  ixxss2  9841  elioc2  9872  divelunit  9938  fzass4  9997  fzrev  10019  fzonmapblen  10122  elfzodifsumelfzo  10136  ssfzo12bi  10160  rebtwn2z  10190  qbtwnxr  10193  modqid  10284  modqcyc  10294  modqaddabs  10297  modqaddmod  10298  mulqaddmodid  10299  modqadd2mod  10309  modqltm1p1mod  10311  modqsubmod  10317  modqsubmodmod  10318  modqmulmod  10324  modqmulmodr  10325  modqsubdir  10328  frecuzrdgg  10351  seq3val  10393  seqvalcd  10394  seq3feq  10407  seq3f1olemp  10437  expp1  10462  expcl2lemap  10467  expnegzap  10489  expadd  10497  expmul  10500  leexp1a  10510  expnlbnd  10579  nn0ltexp2  10623  nn0opth2  10637  bcval  10662  bcval5  10676  bcpasc  10679  hashunsng  10720  seq3coll  10755  shftfvalg  10760  shftfval  10763  seq3shft  10780  caucvgrelemrec  10921  resqrexlemdecn  10954  sqrtmul  10977  sqrtdiv  10984  leabs  11016  absexpzap  11022  ltabs  11029  abslt  11030  absle  11031  abssubap0  11032  amgm2  11060  icodiamlt  11122  qdenre  11144  maxleim  11147  maxleastlt  11157  rexico  11163  zmaxcl  11166  minmax  11171  xrmaxleastlt  11197  xrminmax  11206  climuni  11234  cn1lem  11255  iserex  11280  iserle  11283  climserle  11286  climcau  11288  summodclem2a  11322  summodc  11324  isumss  11332  fisumss  11333  fsumadd  11347  isumadd  11372  fsum2dlemstep  11375  fsum2d  11376  fisum0diag2  11388  fsumabs  11406  isumsplit  11432  geolim  11452  geo2lim  11457  geoisum  11458  geoisumr  11459  geoisum1  11460  mertenslemub  11475  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodmodclem2  11518  prodmodc  11519  zproddc  11520  fprodseq  11524  fprodcl2lem  11546  fprod2dlemstep  11563  fprodle  11581  fprodmodd  11582  efcvgfsum  11608  eftlcl  11629  reeftlcl  11630  tanaddap  11680  zdvdsdc  11752  dvds2ln  11764  dvdsle  11782  divconjdvds  11787  dvdsext  11793  gcdsupex  11890  gcdsupcl  11891  bezoutlemmain  11931  bezoutlemaz  11936  bezoutlembi  11938  bezout  11944  gcdmultiplez  11954  dvdsmulgcd  11958  bezoutr  11965  bezoutr1  11966  lcmval  11995  lcmcllem  11999  ncoprmgcdne1b  12021  cncongr1  12035  isprm5  12074  prmdvdsexp  12080  sqrt2irr  12094  pw2dvdslemn  12097  pw2dvdseu  12100  nonsq  12139  powm2modprm  12184  pcmul  12233  pcqmul  12235  pcexp  12241  pcneg  12256  pcdvdstr  12258  pcprmpw2  12264  pcfac  12280  expnprm  12283  prmpwdvds  12285  mul4sq  12324  ssnnctlemct  12379  infpn2  12389  isstruct2r  12405  setsfun  12429  setsfun0  12430  neissex  12805  tgrest  12809  ssrest  12822  restopn2  12823  cnco  12861  cnss1  12866  cnss2  12867  cnptopresti  12878  uptx  12914  txrest  12916  psmetres2  12973  xmetres2  13019  xblss2ps  13044  blhalf  13048  blssexps  13069  blssex  13070  blin2  13072  blbas  13073  bdmetval  13140  metcnpi  13155  metcnpi2  13156  qtopbas  13162  tgqioo  13187  cncfss  13210  mulc1cncf  13216  cncfmptid  13223  dedekindicc  13251  ivthdec  13262  cnplimcim  13276  cnplimclemle  13277  cnplimccntop  13279  limccnp2cntop  13286  dvfgg  13297  dvcj  13313  dvrecap  13317  dveflem  13327  eflt  13336  ptolemy  13385  cos11  13414  cxplt  13476  cxple  13477  cxplt3  13480  apcxp2  13498  rprelogbmul  13513  rprelogbdiv  13515  lgsval2lem  13551  lgsdir2lem5  13573  2sqlem6  13596  pwtrufal  13877  nninfalllem1  13888  nninfsellemqall  13895  sbthom  13905  qdencn  13906  isomninnlem  13909  trirec0  13923  apdiff  13927  iswomninnlem  13928  ismkvnnlem  13931