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  1086  simp2ll  1090  simp3ll  1094  rmob  3125  ifnefals  3650  prneimg  3857  exmid01  4288  pwntru  4289  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  poinxp  4795  mpteqb  5737  fvmptt  5738  fcof1  5924  acexmid  6017  dftpos4  6429  tfrlem3ag  6475  tfrlem3a  6476  tfrlemi1  6498  tfrexlem  6500  tfr1onlem3ag  6503  nntr2  6671  dcdifsnid  6672  qsel  6781  ecopovsymg  6803  ecopoverg  6805  th3qlem1  6806  mapss  6860  xpmapenlem  7035  findcard2  7078  findcard2s  7079  findcard2sd  7081  unfiin  7118  f1finf1o  7146  fidcenumlemrk  7153  fidcenumlemr  7154  fidcenum  7155  sbthlemi6  7161  sbthlemi8  7163  elfi2  7171  supisolem  7207  enumct  7314  nninfninc  7322  ismkvnex  7354  exmidontriimlem4  7439  netap  7473  2omotaplemap  7476  cc2lem  7485  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  distrnqg  7607  ltexnqq  7628  subhalfnqq  7634  prarloclemarch  7638  nnnq0lem1  7666  distrnq0  7679  npsspw  7691  prarloclemlo  7714  prarloclem3  7717  prarloclemcalc  7722  genplt2i  7730  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  ltexprlemlol  7822  ltexprlemupu  7824  addextpr  7841  recexprlemopl  7845  recexprlemdisj  7850  recexprlem1ssl  7853  aptiprleml  7859  prsrlem1  7962  recexgt0sr  7993  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axaddcl  8084  axmulcl  8086  axmulcom  8091  rereceu  8109  mpomulf  8169  ltntri  8307  cnegexlem1  8354  cnegex  8357  addsub4  8422  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  rereim  8766  apreim  8783  mulreim  8784  addext  8790  mulext  8794  receuap  8849  rec11ap  8890  rec11rap  8891  divdivdivap  8893  ddcanap  8906  divadddivap  8907  divsubdivap  8908  conjmulap  8909  rerecclap  8910  subrecap  9019  recgt0  9030  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  ltmul12a  9040  lemul12a  9042  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  lt2msq  9066  ltrec1  9068  le2msq  9081  msq11  9082  ledivp1  9083  mulle0r  9124  peano5uzti  9588  eluzuzle  9764  qreccl  9876  elpq  9883  xrltso  10031  z2ge  10061  xpncan  10106  xaddge0  10113  xle2add  10114  xleaddadd  10122  ixxss1  10139  ixxss2  10140  elioc2  10171  divelunit  10237  fzass4  10297  fzrev  10319  fzonmapblen  10427  elfzodifsumelfzo  10447  ssfzo12bi  10471  rebtwn2z  10515  qbtwnxr  10518  modqid  10612  modqcyc  10622  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqadd2mod  10637  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modqmulmod  10652  modqmulmodr  10653  modqsubdir  10656  frecuzrdgg  10679  nninfinf  10706  seq3val  10723  seqvalcd  10724  seq3feq  10743  seq3f1olemp  10778  seqfeq4g  10794  expp1  10809  expcl2lemap  10814  expnegzap  10836  expadd  10844  expmul  10847  leexp1a  10857  expnlbnd  10927  nn0ltexp2  10972  nn0opth2  10987  bcval  11012  bcval5  11026  bcpasc  11029  hashunsng  11072  seq3coll  11107  iswrdiz  11124  sswrd  11126  ccatalpha  11194  ccatw2s1p1g  11226  swrdwrdsymbg  11249  swrdsb0eq  11250  ccatswrd  11255  pfxf  11267  pfxwrdsymbg  11275  wrd2ind  11308  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  shftfvalg  11396  shftfval  11399  seq3shft  11416  caucvgrelemrec  11557  resqrexlemdecn  11590  sqrtmul  11613  sqrtdiv  11620  leabs  11652  absexpzap  11658  ltabs  11665  abslt  11666  absle  11667  abssubap0  11668  amgm2  11696  icodiamlt  11758  qdenre  11780  maxleim  11783  maxleastlt  11793  rexico  11799  zmaxcl  11802  minmax  11808  xrmaxleastlt  11834  xrminmax  11843  climuni  11871  cn1lem  11892  iserex  11917  iserle  11920  climserle  11923  climcau  11925  summodclem2a  11960  summodc  11962  isumss  11970  fisumss  11971  fsumadd  11985  isumadd  12010  fsum2dlemstep  12013  fsum2d  12014  fisum0diag2  12026  fsumabs  12044  isumsplit  12070  geolim  12090  geo2lim  12095  geoisum  12096  geoisumr  12097  geoisum1  12098  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodmodclem2  12156  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodcl2lem  12184  fprod2dlemstep  12201  fprodle  12219  fprodmodd  12220  efcvgfsum  12246  eftlcl  12267  reeftlcl  12268  tanaddap  12318  zdvdsdc  12391  dvds2ln  12403  dvdsle  12423  divconjdvds  12428  dvdsext  12434  bitsfzo  12534  gcdsupex  12546  gcdsupcl  12547  bezoutlemmain  12587  bezoutlemaz  12592  bezoutlembi  12594  bezout  12600  gcdmultiplez  12610  dvdsmulgcd  12614  bezoutr  12621  bezoutr1  12622  lcmval  12653  lcmcllem  12657  ncoprmgcdne1b  12679  cncongr1  12693  isprm5  12732  prmdvdsexp  12738  sqrt2irr  12752  pw2dvdslemn  12755  pw2dvdseu  12758  nonsq  12797  powm2modprm  12843  pcmul  12892  pcqmul  12894  pcexp  12900  pcneg  12916  pcdvdstr  12918  pcprmpw2  12924  pcfac  12941  expnprm  12944  prmpwdvds  12946  mul4sq  12985  ssnnctlemct  13085  infpn2  13095  isstruct2r  13111  setsfun  13135  setsfun0  13136  ismndd  13538  submnd0  13545  mhmf1o  13571  resmhm  13588  mhmco  13591  mhmima  13592  dfgrp2  13628  grprcan  13638  grplmulf1o  13675  grplactcnv  13703  pwssub  13714  mhmmnd  13721  mulgval  13727  mulgz  13755  mulgnn0dir  13757  mulgdir  13759  mulgneg2  13761  mhmmulg  13768  issubg4m  13798  nmzsubg  13815  ssnmz  13816  ghmmhmb  13859  resghm  13865  ghmpreima  13871  ghmnsgpreima  13874  ghmf1o  13880  eqgabl  13935  gsumfzconst  13946  rngpropd  13987  srglmhm  14025  srgrmhm  14026  isring  14032  ringadd2  14059  ringpropd  14070  ringlghm  14093  ringrghm  14094  oppr1g  14114  dvdsrex  14131  dvdsrtr  14134  issubrg  14254  unitrrg  14300  islmod  14324  islmodd  14326  lmodfopne  14359  lmodprop2d  14381  lssvacl  14398  lssvsubcl  14399  lssvscl  14408  islss3  14412  lsslss  14414  lss1d  14416  lsspropdg  14464  dflidl2rng  14514  gsumfzfsumlemm  14620  expghmap  14640  mulgghm2  14641  znval  14669  znunit  14692  znrrg  14693  psrbaglesuppg  14705  mplvalcoe  14723  neissex  14908  tgrest  14912  ssrest  14925  restopn2  14926  cnco  14964  cnss1  14969  cnss2  14970  cnptopresti  14981  uptx  15017  txrest  15019  psmetres2  15076  xmetres2  15122  xblss2ps  15147  blhalf  15151  blssexps  15172  blssex  15173  blin2  15175  blbas  15176  bdmetval  15243  metcnpi  15258  metcnpi2  15259  qtopbas  15265  tgqioo  15298  cncfss  15326  mulc1cncf  15332  cncfmptid  15340  dedekindicc  15376  ivthdec  15387  cnplimcim  15410  cnplimclemle  15411  cnplimccntop  15413  limccnp2cntop  15420  dvfgg  15431  dvcj  15452  dvrecap  15456  dvmptfsum  15468  dveflem  15469  elply2  15478  ply1termlem  15485  plymullem1  15491  eflt  15518  ptolemy  15567  cos11  15596  rpcxpmul2  15656  cxplt  15659  cxple  15660  cxplt3  15663  apcxp2  15682  rprelogbmul  15698  rprelogbdiv  15700  sgmval  15726  sgmval2  15727  sgmf  15729  sgmmul  15739  perfect  15744  lgsval2lem  15758  lgsdir2lem5  15780  2sqlem6  15868  umgrnloopv  15984  upgredg  16014  usgr1eop  16115  upgredginwlk  16226  wlkv0  16239  clwwlkccatlem  16270  2omap  16645  pw1map  16647  pwtrufal  16649  nninfalllem1  16661  nninfsellemqall  16668  nnnninfex  16675  sbthom  16681  qdencn  16682  isomninnlem  16685  trirec0  16699  apdiff  16703  qdiff  16704  iswomninnlem  16705  ismkvnnlem  16708  ltlenmkv  16726