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  1087  simp2ll  1091  simp3ll  1095  rmob  3139  ifnefals  3671  ifeqeqxdc  3673  prneimg  3883  exmid01  4316  pwntru  4317  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  poinxp  4824  mpteqb  5773  fvmptt  5774  fcof1  5962  acexmid  6057  fsuppeqg  6461  fvn0elsupp  6464  suppssdc  6473  suppssfvg  6476  dftpos4  6507  tfrlem3ag  6553  tfrlem3a  6554  tfrlemi1  6576  tfrexlem  6578  tfr1onlem3ag  6581  nntr2  6749  dcdifsnid  6750  qsel  6859  ecopovsymg  6881  ecopoverg  6883  th3qlem1  6884  mapss  6939  xpmapenlem  7115  findcard2  7159  findcard2s  7160  findcard2sd  7162  unfiin  7199  f1finf1o  7230  fidcenumlemrk  7237  fidcenumlemr  7238  fidcenum  7239  sbthlemi6  7245  sbthlemi8  7247  elfi2  7272  2omap  7282  2omapfi  7284  supisolem  7312  enumct  7419  nninfninc  7427  ismkvnex  7459  exmidontriimlem4  7544  netap  7584  2omotaplemap  7587  cc2lem  7596  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  distrnqg  7718  ltexnqq  7739  subhalfnqq  7745  prarloclemarch  7749  nnnq0lem1  7777  distrnq0  7790  npsspw  7802  prarloclemlo  7825  prarloclem3  7828  prarloclemcalc  7833  genplt2i  7841  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  ltexprlemlol  7933  ltexprlemupu  7935  addextpr  7952  recexprlemopl  7956  recexprlemdisj  7961  recexprlem1ssl  7964  aptiprleml  7970  prsrlem1  8073  recexgt0sr  8104  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axaddcl  8195  axmulcl  8197  axmulcom  8202  rereceu  8220  mpomulf  8280  ltntri  8417  cnegexlem1  8464  cnegex  8467  addsub4  8532  le2add  8735  lt2add  8736  lt2sub  8751  le2sub  8752  rereim  8877  apreim  8894  mulreim  8895  addext  8901  mulext  8905  receuap  8960  rec11ap  9001  rec11rap  9002  divdivdivap  9004  ddcanap  9017  divadddivap  9018  divsubdivap  9019  conjmulap  9020  rerecclap  9021  subrecap  9130  recgt0  9141  prodgt0gt0  9142  prodgt0  9143  prodge0  9145  ltmul12a  9151  lemul12a  9153  lemulge11  9157  lt2mul2div  9170  ltrec  9174  lerec  9175  lt2msq  9177  ltrec1  9179  le2msq  9192  msq11  9193  ledivp1  9194  mulle0r  9235  peano5uzti  9704  eluzuzle  9880  qreccl  9992  elpq  9999  xrltso  10148  z2ge  10178  xpncan  10223  xaddge0  10230  xle2add  10231  xleaddadd  10239  ixxss1  10256  ixxss2  10257  elioc2  10288  divelunit  10354  fzass4  10417  fzrev  10440  fzonmapblen  10548  elfzodifsumelfzo  10568  ssfzo12bi  10592  rebtwn2z  10638  qbtwnxr  10641  modqid  10735  modqcyc  10745  modqaddabs  10748  modqaddmod  10749  mulqaddmodid  10750  modqadd2mod  10760  modqltm1p1mod  10762  modqsubmod  10768  modqsubmodmod  10769  modqmulmod  10775  modqmulmodr  10776  modqsubdir  10779  frecuzrdgg  10802  nninfinf  10829  seq3val  10846  seqvalcd  10847  seq3feq  10866  seq3f1olemp  10901  seqfeq4g  10917  expp1  10932  expcl2lemap  10937  expnegzap  10959  expadd  10967  expmul  10970  leexp1a  10980  resq01  11044  expnlbnd  11051  nn0ltexp2  11096  nn0opth2  11111  bcval  11136  bcval5  11150  bcpasc  11153  hashunsng  11197  sseqn  11228  hashfibclem  11231  hashfibc  11232  seq3coll  11239  iswrdiz  11256  sswrd  11258  ccatalpha  11326  ccatw2s1p1g  11358  swrdwrdsymbg  11381  swrdsb0eq  11382  ccatswrd  11387  pfxf  11399  pfxwrdsymbg  11407  wrd2ind  11440  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  shftfvalg  11528  shftfval  11531  seq3shft  11548  caucvgrelemrec  11689  resqrexlemdecn  11722  sqrtmul  11745  sqrtdiv  11752  leabs  11784  absexpzap  11790  ltabs  11797  abslt  11798  absle  11799  abssubap0  11800  amgm2  11828  icodiamlt  11890  qdenre  11912  maxleim  11915  maxleastlt  11925  rexico  11931  zmaxcl  11934  minmax  11940  xrmaxleastlt  11966  xrminmax  11975  climuni  12003  cn1lem  12024  iserex  12049  iserle  12052  climserle  12055  climcau  12057  summodclem2a  12092  summodc  12094  isumss  12102  fisumss  12103  fsumadd  12117  isumadd  12142  fsum2dlemstep  12145  fsum2d  12146  fisum0diag2  12158  fsumabs  12176  isumsplit  12202  geolim  12222  geo2lim  12227  geoisum  12228  geoisumr  12229  geoisum1  12230  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodcl2lem  12316  fprod2dlemstep  12333  fprodle  12351  fprodmodd  12352  efcvgfsum  12378  eftlcl  12399  reeftlcl  12400  tanaddap  12450  zdvdsdc  12523  dvds2ln  12535  dvdsle  12555  divconjdvds  12560  dvdsext  12566  bitsfzo  12666  gcdsupex  12678  gcdsupcl  12679  bezoutlemmain  12719  bezoutlemaz  12724  bezoutlembi  12726  bezout  12732  gcdmultiplez  12742  dvdsmulgcd  12746  bezoutr  12753  bezoutr1  12754  lcmval  12785  lcmcllem  12789  ncoprmgcdne1b  12811  cncongr1  12825  isprm5  12864  prmdvdsexp  12870  sqrt2irr  12884  pw2dvdslemn  12887  pw2dvdseu  12890  nonsq  12929  powm2modprm  12975  pcmul  13024  pcqmul  13026  pcexp  13032  pcneg  13048  pcdvdstr  13050  pcprmpw2  13056  pcfac  13073  expnprm  13076  prmpwdvds  13078  mul4sq  13117  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsima  13203  ssnnctlemct  13281  infpn2  13291  isstruct2r  13307  setsfun  13331  setsfun0  13332  ismndd  13698  submnd0  13705  mhmf1o  13725  resmhm  13742  mhmco  13745  mhmima  13746  dfgrp2  13782  grprcan  13792  grplmulf1o  13829  grplactcnv  13857  mhmmnd  13869  mulgval  13875  mulgz  13903  mulgnn0dir  13905  mulgdir  13907  mulgneg2  13909  mhmmulg  13916  issubg4m  13946  nmzsubg  13963  ssnmz  13964  ghmmhmb  14007  resghm  14013  ghmpreima  14019  ghmnsgpreima  14022  ghmf1o  14028  eqgabl  14083  gsumfzconst  14094  pwssub  14158  rngpropd  14194  srglmhm  14236  srgrmhm  14237  isring  14243  ringadd2  14270  ringpropd  14281  ringlghm  14304  ringrghm  14305  oppr1g  14326  dvdsrex  14343  dvdsrtr  14346  issubrg  14467  unitrrg  14514  aprnzr  14537  opprdrng  14558  islmod  14565  islmodd  14567  lmodfopne  14600  lmodprop2d  14622  lssvacl  14639  lssvsubcl  14640  lssvscl  14649  islss3  14653  lsslss  14655  lss1d  14657  lsspropdg  14705  dflidl2rng  14755  gsumfzfsumlemm  14861  expghmap  14881  mulgghm2  14882  znval  14910  znunit  14933  znrrg  14934  psrbaglesuppg  14947  mplvalcoe  14971  neissex  15156  tgrest  15160  ssrest  15173  restopn2  15174  cnco  15212  cnss1  15217  cnss2  15218  cnptopresti  15229  uptx  15265  txrest  15267  psmetres2  15324  xmetres2  15370  xblss2ps  15395  blhalf  15399  blssexps  15420  blssex  15421  blin2  15423  blbas  15424  bdmetval  15491  metcnpi  15506  metcnpi2  15507  qtopbas  15513  tgqioo  15546  cncfss  15574  mulc1cncf  15580  cncfmptid  15588  dedekindicc  15624  ivthdec  15635  cnplimcim  15658  cnplimclemle  15659  cnplimccntop  15661  limccnp2cntop  15668  dvfgg  15679  dvcj  15700  dvrecap  15704  dvmptfsum  15716  dveflem  15717  elply2  15726  ply1termlem  15733  plymullem1  15739  eflt  15766  ptolemy  15815  cos11  15844  rpcxpmul2  15904  cxplt  15907  cxple  15908  cxplt3  15911  apcxp2  15930  rprelogbmul  15946  rprelogbdiv  15948  pellexlem3  15973  sgmval  15977  sgmval2  15978  sgmf  15980  sgmmul  15990  perfect  15995  lgsval2lem  16009  lgsdir2lem5  16031  2sqlem6  16119  umgrnloopv  16235  upgredg  16265  usgr1eop  16366  upgredginwlk  16477  wlkv0  16490  clwwlkccatlem  16521  pw1map  16895  pwtrufal  16897  nninfalllem1  16912  nninfsellemqall  16919  nnnninfex  16926  sbthom  16932  qdencn  16933  isomninnlem  16940  trirec0  16954  apdiff  16958  qdiff  16959  iswomninnlem  16960  ismkvnnlem  16963  ltlenmkv  16982