Theorem simpll 524

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 485	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  1055  simp2ll  1059  simp3ll  1063  rmob  3047  prneimg  3761  exmid01  4184  pwntru  4185  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  poinxp  4680  mpteqb  5586  fvmptt  5587  fcof1  5762  acexmid  5852  dftpos4  6242  tfrlem3ag  6288  tfrlem3a  6289  tfrlemi1  6311  tfrexlem  6313  tfr1onlem3ag  6316  nntr2  6482  dcdifsnid  6483  qsel  6590  ecopovsymg  6612  ecopoverg  6614  th3qlem1  6615  mapss  6669  xpmapenlem  6827  findcard2  6867  findcard2s  6868  findcard2sd  6870  unfiin  6903  f1finf1o  6924  fidcenumlemrk  6931  fidcenumlemr  6932  fidcenum  6933  sbthlemi6  6939  sbthlemi8  6941  elfi2  6949  supisolem  6985  enumct  7092  ismkvnex  7131  exmidontriimlem4  7201  cc2lem  7228  dfplpq2  7316  dfmpq2  7317  mulpipqqs  7335  distrnqg  7349  ltexnqq  7370  subhalfnqq  7376  prarloclemarch  7380  nnnq0lem1  7408  distrnq0  7421  npsspw  7433  prarloclemlo  7456  prarloclem3  7459  prarloclemcalc  7464  genplt2i  7472  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  ltprordil  7551  ltexprlemlol  7564  ltexprlemupu  7566  addextpr  7583  recexprlemopl  7587  recexprlemdisj  7592  recexprlem1ssl  7595  aptiprleml  7601  prsrlem1  7704  recexgt0sr  7735  addcnsr  7796  mulcnsr  7797  mulcnsrec  7805  axaddcl  7826  axmulcl  7828  axmulcom  7833  rereceu  7851  ltntri  8047  cnegexlem1  8094  cnegex  8097  addsub4  8162  le2add  8363  lt2add  8364  lt2sub  8379  le2sub  8380  rereim  8505  apreim  8522  mulreim  8523  addext  8529  mulext  8533  receuap  8587  rec11ap  8627  rec11rap  8628  divdivdivap  8630  ddcanap  8643  divadddivap  8644  divsubdivap  8645  conjmulap  8646  rerecclap  8647  subrecap  8756  recgt0  8766  prodgt0gt0  8767  prodgt0  8768  prodge0  8770  ltmul12a  8776  lemul12a  8778  lemulge11  8782  lt2mul2div  8795  ltrec  8799  lerec  8800  lt2msq  8802  ltrec1  8804  le2msq  8817  msq11  8818  ledivp1  8819  mulle0r  8860  peano5uzti  9320  eluzuzle  9495  qreccl  9601  elpq  9607  xrltso  9753  z2ge  9783  xpncan  9828  xaddge0  9835  xle2add  9836  xleaddadd  9844  ixxss1  9861  ixxss2  9862  elioc2  9893  divelunit  9959  fzass4  10018  fzrev  10040  fzonmapblen  10143  elfzodifsumelfzo  10157  ssfzo12bi  10181  rebtwn2z  10211  qbtwnxr  10214  modqid  10305  modqcyc  10315  modqaddabs  10318  modqaddmod  10319  mulqaddmodid  10320  modqadd2mod  10330  modqltm1p1mod  10332  modqsubmod  10338  modqsubmodmod  10339  modqmulmod  10345  modqmulmodr  10346  modqsubdir  10349  frecuzrdgg  10372  seq3val  10414  seqvalcd  10415  seq3feq  10428  seq3f1olemp  10458  expp1  10483  expcl2lemap  10488  expnegzap  10510  expadd  10518  expmul  10521  leexp1a  10531  expnlbnd  10600  nn0ltexp2  10644  nn0opth2  10658  bcval  10683  bcval5  10697  bcpasc  10700  hashunsng  10742  seq3coll  10777  shftfvalg  10782  shftfval  10785  seq3shft  10802  caucvgrelemrec  10943  resqrexlemdecn  10976  sqrtmul  10999  sqrtdiv  11006  leabs  11038  absexpzap  11044  ltabs  11051  abslt  11052  absle  11053  abssubap0  11054  amgm2  11082  icodiamlt  11144  qdenre  11166  maxleim  11169  maxleastlt  11179  rexico  11185  zmaxcl  11188  minmax  11193  xrmaxleastlt  11219  xrminmax  11228  climuni  11256  cn1lem  11277  iserex  11302  iserle  11305  climserle  11308  climcau  11310  summodclem2a  11344  summodc  11346  isumss  11354  fisumss  11355  fsumadd  11369  isumadd  11394  fsum2dlemstep  11397  fsum2d  11398  fisum0diag2  11410  fsumabs  11428  isumsplit  11454  geolim  11474  geo2lim  11479  geoisum  11480  geoisumr  11481  geoisum1  11482  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodcl2lem  11568  fprod2dlemstep  11585  fprodle  11603  fprodmodd  11604  efcvgfsum  11630  eftlcl  11651  reeftlcl  11652  tanaddap  11702  zdvdsdc  11774  dvds2ln  11786  dvdsle  11804  divconjdvds  11809  dvdsext  11815  gcdsupex  11912  gcdsupcl  11913  bezoutlemmain  11953  bezoutlemaz  11958  bezoutlembi  11960  bezout  11966  gcdmultiplez  11976  dvdsmulgcd  11980  bezoutr  11987  bezoutr1  11988  lcmval  12017  lcmcllem  12021  ncoprmgcdne1b  12043  cncongr1  12057  isprm5  12096  prmdvdsexp  12102  sqrt2irr  12116  pw2dvdslemn  12119  pw2dvdseu  12122  nonsq  12161  powm2modprm  12206  pcmul  12255  pcqmul  12257  pcexp  12263  pcneg  12278  pcdvdstr  12280  pcprmpw2  12286  pcfac  12302  expnprm  12305  prmpwdvds  12307  mul4sq  12346  ssnnctlemct  12401  infpn2  12411  isstruct2r  12427  setsfun  12451  setsfun0  12452  ismndd  12673  mhmf1o  12693  mhmco  12705  mhmima  12706  dfgrp2  12732  grprcan  12740  neissex  12959  tgrest  12963  ssrest  12976  restopn2  12977  cnco  13015  cnss1  13020  cnss2  13021  cnptopresti  13032  uptx  13068  txrest  13070  psmetres2  13127  xmetres2  13173  xblss2ps  13198  blhalf  13202  blssexps  13223  blssex  13224  blin2  13226  blbas  13227  bdmetval  13294  metcnpi  13309  metcnpi2  13310  qtopbas  13316  tgqioo  13341  cncfss  13364  mulc1cncf  13370  cncfmptid  13377  dedekindicc  13405  ivthdec  13416  cnplimcim  13430  cnplimclemle  13431  cnplimccntop  13433  limccnp2cntop  13440  dvfgg  13451  dvcj  13467  dvrecap  13471  dveflem  13481  eflt  13490  ptolemy  13539  cos11  13568  cxplt  13630  cxple  13631  cxplt3  13634  apcxp2  13652  rprelogbmul  13667  rprelogbdiv  13669  lgsval2lem  13705  lgsdir2lem5  13727  2sqlem6  13750  pwtrufal  14030  nninfalllem1  14041  nninfsellemqall  14048  sbthom  14058  qdencn  14059  isomninnlem  14062  trirec0  14076  apdiff  14080  iswomninnlem  14081  ismkvnnlem  14084