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  3078  ifnefals  3599  prneimg  3800  exmid01  4227  pwntru  4228  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  poinxp  4728  mpteqb  5648  fvmptt  5649  fcof1  5826  acexmid  5917  dftpos4  6316  tfrlem3ag  6362  tfrlem3a  6363  tfrlemi1  6385  tfrexlem  6387  tfr1onlem3ag  6390  nntr2  6556  dcdifsnid  6557  qsel  6666  ecopovsymg  6688  ecopoverg  6690  th3qlem1  6691  mapss  6745  xpmapenlem  6905  findcard2  6945  findcard2s  6946  findcard2sd  6948  unfiin  6982  f1finf1o  7006  fidcenumlemrk  7013  fidcenumlemr  7014  fidcenum  7015  sbthlemi6  7021  sbthlemi8  7023  elfi2  7031  supisolem  7067  enumct  7174  nninfninc  7182  ismkvnex  7214  exmidontriimlem4  7284  netap  7314  2omotaplemap  7317  cc2lem  7326  dfplpq2  7414  dfmpq2  7415  mulpipqqs  7433  distrnqg  7447  ltexnqq  7468  subhalfnqq  7474  prarloclemarch  7478  nnnq0lem1  7506  distrnq0  7519  npsspw  7531  prarloclemlo  7554  prarloclem3  7557  prarloclemcalc  7562  genplt2i  7570  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  ltprordil  7649  ltexprlemlol  7662  ltexprlemupu  7664  addextpr  7681  recexprlemopl  7685  recexprlemdisj  7690  recexprlem1ssl  7693  aptiprleml  7699  prsrlem1  7802  recexgt0sr  7833  addcnsr  7894  mulcnsr  7895  mulcnsrec  7903  axaddcl  7924  axmulcl  7926  axmulcom  7931  rereceu  7949  mpomulf  8009  ltntri  8147  cnegexlem1  8194  cnegex  8197  addsub4  8262  le2add  8463  lt2add  8464  lt2sub  8479  le2sub  8480  rereim  8605  apreim  8622  mulreim  8623  addext  8629  mulext  8633  receuap  8688  rec11ap  8729  rec11rap  8730  divdivdivap  8732  ddcanap  8745  divadddivap  8746  divsubdivap  8747  conjmulap  8748  rerecclap  8749  subrecap  8858  recgt0  8869  prodgt0gt0  8870  prodgt0  8871  prodge0  8873  ltmul12a  8879  lemul12a  8881  lemulge11  8885  lt2mul2div  8898  ltrec  8902  lerec  8903  lt2msq  8905  ltrec1  8907  le2msq  8920  msq11  8921  ledivp1  8922  mulle0r  8963  peano5uzti  9425  eluzuzle  9600  qreccl  9707  elpq  9714  xrltso  9862  z2ge  9892  xpncan  9937  xaddge0  9944  xle2add  9945  xleaddadd  9953  ixxss1  9970  ixxss2  9971  elioc2  10002  divelunit  10068  fzass4  10128  fzrev  10150  fzonmapblen  10254  elfzodifsumelfzo  10268  ssfzo12bi  10292  rebtwn2z  10323  qbtwnxr  10326  modqid  10420  modqcyc  10430  modqaddabs  10433  modqaddmod  10434  mulqaddmodid  10435  modqadd2mod  10445  modqltm1p1mod  10447  modqsubmod  10453  modqsubmodmod  10454  modqmulmod  10460  modqmulmodr  10461  modqsubdir  10464  frecuzrdgg  10487  nninfinf  10514  seq3val  10531  seqvalcd  10532  seq3feq  10551  seq3f1olemp  10586  seqfeq4g  10602  expp1  10617  expcl2lemap  10622  expnegzap  10644  expadd  10652  expmul  10655  leexp1a  10665  expnlbnd  10735  nn0ltexp2  10780  nn0opth2  10795  bcval  10820  bcval5  10834  bcpasc  10837  hashunsng  10878  seq3coll  10913  iswrdiz  10921  sswrd  10923  shftfvalg  10962  shftfval  10965  seq3shft  10982  caucvgrelemrec  11123  resqrexlemdecn  11156  sqrtmul  11179  sqrtdiv  11186  leabs  11218  absexpzap  11224  ltabs  11231  abslt  11232  absle  11233  abssubap0  11234  amgm2  11262  icodiamlt  11324  qdenre  11346  maxleim  11349  maxleastlt  11359  rexico  11365  zmaxcl  11368  minmax  11373  xrmaxleastlt  11399  xrminmax  11408  climuni  11436  cn1lem  11457  iserex  11482  iserle  11485  climserle  11488  climcau  11490  summodclem2a  11524  summodc  11526  isumss  11534  fisumss  11535  fsumadd  11549  isumadd  11574  fsum2dlemstep  11577  fsum2d  11578  fisum0diag2  11590  fsumabs  11608  isumsplit  11634  geolim  11654  geo2lim  11659  geoisum  11660  geoisumr  11661  geoisum1  11662  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodcl2lem  11748  fprod2dlemstep  11765  fprodle  11783  fprodmodd  11784  efcvgfsum  11810  eftlcl  11831  reeftlcl  11832  tanaddap  11882  zdvdsdc  11955  dvds2ln  11967  dvdsle  11986  divconjdvds  11991  dvdsext  11997  gcdsupex  12094  gcdsupcl  12095  bezoutlemmain  12135  bezoutlemaz  12140  bezoutlembi  12142  bezout  12148  gcdmultiplez  12158  dvdsmulgcd  12162  bezoutr  12169  bezoutr1  12170  lcmval  12201  lcmcllem  12205  ncoprmgcdne1b  12227  cncongr1  12241  isprm5  12280  prmdvdsexp  12286  sqrt2irr  12300  pw2dvdslemn  12303  pw2dvdseu  12306  nonsq  12345  powm2modprm  12390  pcmul  12439  pcqmul  12441  pcexp  12447  pcneg  12463  pcdvdstr  12465  pcprmpw2  12471  pcfac  12488  expnprm  12491  prmpwdvds  12493  mul4sq  12532  ssnnctlemct  12603  infpn2  12613  isstruct2r  12629  setsfun  12653  setsfun0  12654  ismndd  13018  submnd0  13025  mhmf1o  13042  resmhm  13059  mhmco  13062  mhmima  13063  dfgrp2  13099  grprcan  13109  grplmulf1o  13146  grplactcnv  13174  mhmmnd  13186  mulgval  13192  mulgz  13220  mulgnn0dir  13222  mulgdir  13224  mulgneg2  13226  mhmmulg  13233  issubg4m  13263  nmzsubg  13280  ssnmz  13281  ghmmhmb  13324  resghm  13330  ghmpreima  13336  ghmnsgpreima  13339  ghmf1o  13345  eqgabl  13400  gsumfzconst  13411  rngpropd  13451  srglmhm  13489  srgrmhm  13490  isring  13496  ringadd2  13523  ringpropd  13534  ringlghm  13557  ringrghm  13558  oppr1g  13578  dvdsrex  13594  dvdsrtr  13597  issubrg  13717  unitrrg  13763  islmod  13787  islmodd  13789  lmodfopne  13822  lmodprop2d  13844  lssvacl  13861  lssvsubcl  13862  lssvscl  13871  islss3  13875  lsslss  13877  lss1d  13879  lsspropdg  13927  dflidl2rng  13977  gsumfzfsumlemm  14075  expghmap  14095  mulgghm2  14096  znval  14124  znunit  14147  znrrg  14148  psrbaglesuppg  14158  neissex  14333  tgrest  14337  ssrest  14350  restopn2  14351  cnco  14389  cnss1  14394  cnss2  14395  cnptopresti  14406  uptx  14442  txrest  14444  psmetres2  14501  xmetres2  14547  xblss2ps  14572  blhalf  14576  blssexps  14597  blssex  14598  blin2  14600  blbas  14601  bdmetval  14668  metcnpi  14683  metcnpi2  14684  qtopbas  14690  tgqioo  14715  cncfss  14738  mulc1cncf  14744  cncfmptid  14751  dedekindicc  14787  ivthdec  14798  cnplimcim  14821  cnplimclemle  14822  cnplimccntop  14824  limccnp2cntop  14831  dvfgg  14842  dvcj  14858  dvrecap  14862  dveflem  14872  elply2  14881  ply1termlem  14888  plymullem1  14894  eflt  14910  ptolemy  14959  cos11  14988  cxplt  15050  cxple  15051  cxplt3  15054  apcxp2  15072  rprelogbmul  15087  rprelogbdiv  15089  lgsval2lem  15126  lgsdir2lem5  15148  2sqlem6  15207  pwtrufal  15488  nninfalllem1  15498  nninfsellemqall  15505  sbthom  15516  qdencn  15517  isomninnlem  15520  trirec0  15534  apdiff  15538  iswomninnlem  15539  ismkvnnlem  15542  ltlenmkv  15560