Theorem simpll 531

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 492	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp1ll  1091  simp2ll  1095  simp3ll  1099  rmob  3145  ifnefals  3685  ifeqeqxdc  3687  prneimg  3899  exmid01  4337  pwntru  4338  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  poinxp  4846  mpteqb  5799  fvmptt  5800  fcof1  5992  acexmid  6087  fsuppeqg  6492  fvn0elsupp  6495  suppssdc  6504  suppssfvg  6507  dftpos4  6539  tfrlem3ag  6585  tfrlem3a  6586  tfrlemi1  6608  tfrexlem  6610  tfr1onlem3ag  6613  nntr2  6781  dcdifsnid  6782  qsel  6891  ecopovsymg  6913  ecopoverg  6915  th3qlem1  6916  mapss  6979  xpmapenlem  7155  findcard2  7199  findcard2s  7200  findcard2sd  7202  unfiin  7239  f1finf1o  7271  fidcenumlemrk  7278  fidcenumlemr  7279  fidcenum  7280  sbthlemi6  7286  sbthlemi8  7288  elfi2  7311  f1setfi  7322  2omap  7324  2omapfi  7326  supisolem  7354  enumct  7461  nninfninc  7469  ismkvnex  7501  exmidontriimlem4  7586  netap  7626  2omotaplemap  7629  cc2lem  7638  dfplpq2  7727  dfmpq2  7728  mulpipqqs  7746  distrnqg  7760  ltexnqq  7781  subhalfnqq  7787  prarloclemarch  7791  nnnq0lem1  7819  distrnq0  7832  npsspw  7844  prarloclemlo  7867  prarloclem3  7870  prarloclemcalc  7875  genplt2i  7883  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  ltprordil  7962  ltexprlemlol  7975  ltexprlemupu  7977  addextpr  7994  recexprlemopl  7998  recexprlemdisj  8003  recexprlem1ssl  8006  aptiprleml  8012  prsrlem1  8115  recexgt0sr  8146  addcnsr  8207  mulcnsr  8208  mulcnsrec  8216  axaddcl  8237  axmulcl  8239  axmulcom  8244  rereceu  8262  mpomulf  8322  ltntri  8461  cnegexlem1  8508  cnegex  8511  addsub4  8576  le2add  8779  lt2add  8780  lt2sub  8795  le2sub  8796  rereim  8922  apreim  8939  mulreim  8940  addext  8946  mulext  8950  receuap  9007  rec11ap  9048  rec11rap  9049  divdivdivap  9051  ddcanap  9064  divadddivap  9065  divsubdivap  9066  conjmulap  9067  rerecclap  9068  subrecap  9177  recgt0  9188  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  ltmul12a  9198  lemul12a  9200  lemulge11  9204  lt2mul2div  9217  ltrec  9221  lerec  9222  lt2msq  9224  ltrec1  9226  le2msq  9239  msq11  9240  ledivp1  9241  mulle0r  9282  peano5uzti  9764  eluzuzle  9945  qreccl  10057  irraddap  10062  elpq  10065  xrltso  10214  z2ge  10244  xpncan  10289  xaddge0  10296  xle2add  10297  xleaddadd  10305  ixxss1  10322  ixxss2  10323  elioc2  10354  divelunit  10420  fzass4  10484  fzrev  10507  fzonmapblen  10615  elfzodifsumelfzo  10635  ssfzo12bi  10659  rebtwn2z  10705  qbtwnxr  10708  flaplt  10738  modqid  10806  modqcyc  10816  modqaddabs  10819  modqaddmod  10820  mulqaddmodid  10821  modqadd2mod  10831  modqltm1p1mod  10833  modqsubmod  10839  modqsubmodmod  10840  modqmulmod  10846  modqmulmodr  10847  modqsubdir  10850  frecuzrdgg  10873  nninfinf  10900  seq3val  10917  seqvalcd  10918  seq3feq  10937  seq3f1olemp  10972  seqfeq4g  10988  expp1  11003  expcl2lemap  11008  expnegzap  11030  expadd  11038  expmul  11041  leexp1a  11051  resq01  11115  expnlbnd  11122  nn0ltexp2  11168  nn0opth2  11183  bcval  11208  bcval5  11222  bcpasc  11225  hashunsng  11269  sseqn  11300  hashfibclem  11303  hashfibc  11304  hashf1lem2  11307  seq3coll  11315  iswrdiz  11332  sswrd  11334  ccatalpha  11402  ccatw2s1p1g  11434  swrdwrdsymbg  11457  swrdsb0eq  11458  ccatswrd  11463  pfxf  11475  pfxwrdsymbg  11483  wrd2ind  11516  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  shftfvalg  11604  shftfval  11607  seq3shft  11624  caucvgrelemrec  11766  resqrexlemdecn  11799  sqrtmul  11822  sqrtdiv  11829  leabs  11861  absexpzap  11868  ltabs  11875  abslt  11876  absle  11877  abssubap0  11878  amgm2  11906  icodiamlt  11968  qdenre  11990  maxleim  11993  maxleastlt  12003  rexico  12009  zmaxcl  12012  minmax  12019  zmincl  12028  xrmaxleastlt  12046  xrminmax  12055  climuni  12083  cn1lem  12104  iserex  12129  iserle  12132  climserle  12135  climcau  12137  summodclem2a  12172  summodc  12174  isumss  12182  fisumss  12183  fsumadd  12197  isumadd  12222  fsum2dlemstep  12225  fsum2d  12226  fisum0diag2  12238  fsumabs  12256  isumsplit  12282  geolim  12302  geo2lim  12307  geoisum  12308  geoisumr  12309  geoisum1  12310  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodcl2lem  12396  fprod2dlemstep  12413  fprodle  12431  fprodmodd  12432  efcvgfsum  12458  eftlcl  12479  reeftlcl  12480  tanaddap  12530  zdvdsdc  12603  dvds2ln  12615  dvdsle  12635  divconjdvds  12640  dvdsext  12646  bitsfzo  12746  gcdsupex  12758  gcdsupcl  12759  bezoutlemmain  12799  bezoutlemaz  12804  bezoutlembi  12806  bezout  12812  gcdmultiplez  12822  dvdsmulgcd  12826  bezoutr  12833  bezoutr1  12834  lcmval  12865  lcmcllem  12869  ncoprmgcdne1b  12891  cncongr1  12905  isprm5  12945  prmdvdsexp  12951  sqrt2irr  12965  pwbdvdslemn  12968  nonsq  13011  powm2modprm  13059  pcmul  13108  pcqmul  13110  pcexp  13116  pcneg  13132  pcdvdstr  13134  pcprmpw2  13140  pcfac  13157  expnprm  13160  prmpwdvds  13162  mul4sq  13201  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemsima  13316  ssnnctlemct  13394  infpn2  13404  isstruct2r  13420  setsfun  13444  setsfun0  13445  ismndd  13808  submnd0  13815  mhmf1o  13835  resmhm  13852  mhmco  13855  mhmima  13856  dfgrp2  13890  grprcan  13900  grplmulf1o  13937  grplactcnv  13965  mhmmnd  13977  mulgval  13983  mulgz  14011  mulgnn0dir  14013  mulgdir  14015  mulgneg2  14017  mhmmulg  14024  issubg4m  14054  nmzsubg  14071  ssnmz  14072  ghmmhmb  14115  resghm  14121  ghmpreima  14127  ghmnsgpreima  14130  ghmf1o  14136  resscntz  14165  cntzsgrpcl  14166  cntzsubm  14169  cntzsubg  14170  cntzmhm  14172  eqgabl  14223  gzsumconst  14232  gsumsnfdcmn  14256  pwssub  14322  rngpropd  14360  srglmhm  14403  srgrmhm  14404  isring  14410  ringadd2  14438  ringpropd  14449  ringlghm  14472  ringrghm  14473  oppr1g  14496  dvdsrex  14513  dvdsrtr  14516  issubrg  14637  unitrrg  14684  aprnzr  14707  opprdrng  14728  islmod  14735  islmodd  14737  lmodfopne  14771  lmodprop2d  14793  lssvacl  14810  lssvsubcl  14811  lssvscl  14820  islss3  14824  lsslss  14826  lss1d  14828  lsspropdg  14876  dflidl2rng  14926  expghmap  15050  mulgghm2  15051  znval  15079  znunit  15102  znrrg  15103  assapropd  15122  assamulgscmlem1  15149  assamulgscmlem2  15150  psrbaglesuppg  15170  neissex  15408  tgrest  15412  ssrest  15425  restopn2  15426  cnco  15464  cnss1  15469  cnss2  15470  cnptopresti  15481  uptx  15517  txrest  15519  psmetres2  15576  xmetres2  15622  xblss2ps  15647  blhalf  15651  blssexps  15672  blssex  15673  blin2  15675  blbas  15676  bdmetval  15743  metcnpi  15758  metcnpi2  15759  qtopbas  15765  tgqioo  15798  cncfss  15826  mulc1cncf  15832  cncfmptid  15840  dedekindicc  15876  ivthdec  15887  cnplimcim  15910  cnplimclemle  15911  cnplimccntop  15913  limccnp2cntop  15920  dvfgg  15931  dvcj  15952  dvrecap  15956  dvmptfsum  15968  dveflem  15969  elply2  15978  ply1termlem  15985  plymullem1  15991  eflt  16018  ptolemy  16068  cos11  16098  logdivlt  16141  logdivle  16142  rpcxpmul2  16163  rpcxpmul2z  16165  cxplt  16168  cxple  16169  cxplt3  16172  apcxp2  16191  rprelogbmul  16208  rprelogbdiv  16210  birthdaylem3  16244  pellexlem3  16248  efnnfsumcl  16256  sgmval  16269  sgmval2  16270  sgmf  16272  efchtqdvds  16282  sgmmul  16307  perfect  16318  bcmax  16322  bposlem1  16328  bpos  16337  lgsval2lem  16351  lgsdir2lem5  16373  2sqlem6  16461  umgrnloopv  16577  upgredg  16607  usgr1eop  16708  upgredginwlk  16819  wlkv0  16832  clwwlkccatlem  16863  pw1map  17247  pwtrufal  17249  nninfalllem1  17274  nninfsellemqall  17281  nnnninfex  17288  sbthom  17294  qdencn  17295  isomninnlem  17302  trirec0  17317  apdiff  17321  qdiff  17322  iswomninnlem  17323  ismkvnnlem  17326  ltlenmkv  17344