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  4335  pwntru  4336  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  poinxp  4844  mpteqb  5796  fvmptt  5797  fcof1  5989  acexmid  6084  fsuppeqg  6488  fvn0elsupp  6491  suppssdc  6500  suppssfvg  6503  dftpos4  6534  tfrlem3ag  6580  tfrlem3a  6581  tfrlemi1  6603  tfrexlem  6605  tfr1onlem3ag  6608  nntr2  6776  dcdifsnid  6777  qsel  6886  ecopovsymg  6908  ecopoverg  6910  th3qlem1  6911  mapss  6973  xpmapenlem  7149  findcard2  7193  findcard2s  7194  findcard2sd  7196  unfiin  7233  f1finf1o  7264  fidcenumlemrk  7271  fidcenumlemr  7272  fidcenum  7273  sbthlemi6  7279  sbthlemi8  7281  elfi2  7306  f1setfi  7317  2omap  7318  2omapfi  7320  supisolem  7348  enumct  7455  nninfninc  7463  ismkvnex  7495  exmidontriimlem4  7580  netap  7620  2omotaplemap  7623  cc2lem  7632  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  distrnqg  7754  ltexnqq  7775  subhalfnqq  7781  prarloclemarch  7785  nnnq0lem1  7813  distrnq0  7826  npsspw  7838  prarloclemlo  7861  prarloclem3  7864  prarloclemcalc  7869  genplt2i  7877  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  ltexprlemlol  7969  ltexprlemupu  7971  addextpr  7988  recexprlemopl  7992  recexprlemdisj  7997  recexprlem1ssl  8000  aptiprleml  8006  prsrlem1  8109  recexgt0sr  8140  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axaddcl  8231  axmulcl  8233  axmulcom  8238  rereceu  8256  mpomulf  8316  ltntri  8454  cnegexlem1  8501  cnegex  8504  addsub4  8569  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  rereim  8914  apreim  8931  mulreim  8932  addext  8938  mulext  8942  receuap  8999  rec11ap  9040  rec11rap  9041  divdivdivap  9043  ddcanap  9056  divadddivap  9057  divsubdivap  9058  conjmulap  9059  rerecclap  9060  subrecap  9169  recgt0  9180  prodgt0gt0  9181  prodgt0  9182  prodge0  9184  ltmul12a  9190  lemul12a  9192  lemulge11  9196  lt2mul2div  9209  ltrec  9213  lerec  9214  lt2msq  9216  ltrec1  9218  le2msq  9231  msq11  9232  ledivp1  9233  mulle0r  9274  peano5uzti  9754  eluzuzle  9930  qreccl  10042  elpq  10049  xrltso  10198  z2ge  10228  xpncan  10273  xaddge0  10280  xle2add  10281  xleaddadd  10289  ixxss1  10306  ixxss2  10307  elioc2  10338  divelunit  10404  fzass4  10468  fzrev  10491  fzonmapblen  10599  elfzodifsumelfzo  10619  ssfzo12bi  10643  rebtwn2z  10689  qbtwnxr  10692  modqid  10786  modqcyc  10796  modqaddabs  10799  modqaddmod  10800  mulqaddmodid  10801  modqadd2mod  10811  modqltm1p1mod  10813  modqsubmod  10819  modqsubmodmod  10820  modqmulmod  10826  modqmulmodr  10827  modqsubdir  10830  frecuzrdgg  10853  nninfinf  10880  seq3val  10897  seqvalcd  10898  seq3feq  10917  seq3f1olemp  10952  seqfeq4g  10968  expp1  10983  expcl2lemap  10988  expnegzap  11010  expadd  11018  expmul  11021  leexp1a  11031  resq01  11095  expnlbnd  11102  nn0ltexp2  11147  nn0opth2  11162  bcval  11187  bcval5  11201  bcpasc  11204  hashunsng  11248  sseqn  11279  hashfibclem  11282  hashfibc  11283  hashf1lem2  11286  seq3coll  11294  iswrdiz  11311  sswrd  11313  ccatalpha  11381  ccatw2s1p1g  11413  swrdwrdsymbg  11436  swrdsb0eq  11437  ccatswrd  11442  pfxf  11454  pfxwrdsymbg  11462  wrd2ind  11495  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  shftfvalg  11583  shftfval  11586  seq3shft  11603  caucvgrelemrec  11745  resqrexlemdecn  11778  sqrtmul  11801  sqrtdiv  11808  leabs  11840  absexpzap  11846  ltabs  11853  abslt  11854  absle  11855  abssubap0  11856  amgm2  11884  icodiamlt  11946  qdenre  11968  maxleim  11971  maxleastlt  11981  rexico  11987  zmaxcl  11990  minmax  11996  xrmaxleastlt  12022  xrminmax  12031  climuni  12059  cn1lem  12080  iserex  12105  iserle  12108  climserle  12111  climcau  12113  summodclem2a  12148  summodc  12150  isumss  12158  fisumss  12159  fsumadd  12173  isumadd  12198  fsum2dlemstep  12201  fsum2d  12202  fisum0diag2  12214  fsumabs  12232  isumsplit  12258  geolim  12278  geo2lim  12283  geoisum  12284  geoisumr  12285  geoisum1  12286  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodcl2lem  12372  fprod2dlemstep  12389  fprodle  12407  fprodmodd  12408  efcvgfsum  12434  eftlcl  12455  reeftlcl  12456  tanaddap  12506  zdvdsdc  12579  dvds2ln  12591  dvdsle  12611  divconjdvds  12616  dvdsext  12622  bitsfzo  12722  gcdsupex  12734  gcdsupcl  12735  bezoutlemmain  12775  bezoutlemaz  12780  bezoutlembi  12782  bezout  12788  gcdmultiplez  12798  dvdsmulgcd  12802  bezoutr  12809  bezoutr1  12810  lcmval  12841  lcmcllem  12845  ncoprmgcdne1b  12867  cncongr1  12881  isprm5  12920  prmdvdsexp  12926  sqrt2irr  12940  pw2dvdslemn  12943  pw2dvdseu  12946  nonsq  12985  powm2modprm  13031  pcmul  13080  pcqmul  13082  pcexp  13088  pcneg  13104  pcdvdstr  13106  pcprmpw2  13112  pcfac  13129  expnprm  13132  prmpwdvds  13134  mul4sq  13173  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemsima  13259  ssnnctlemct  13337  infpn2  13347  isstruct2r  13363  setsfun  13387  setsfun0  13388  ismndd  13750  submnd0  13757  mhmf1o  13777  resmhm  13794  mhmco  13797  mhmima  13798  dfgrp2  13832  grprcan  13842  grplmulf1o  13879  grplactcnv  13907  mhmmnd  13919  mulgval  13925  mulgz  13953  mulgnn0dir  13955  mulgdir  13957  mulgneg2  13959  mhmmulg  13966  issubg4m  13996  nmzsubg  14013  ssnmz  14014  ghmmhmb  14057  resghm  14063  ghmpreima  14069  ghmnsgpreima  14072  ghmf1o  14078  eqgabl  14134  gzsumconst  14143  pwssub  14216  rngpropd  14254  srglmhm  14297  srgrmhm  14298  isring  14304  ringadd2  14332  ringpropd  14343  ringlghm  14366  ringrghm  14367  oppr1g  14388  dvdsrex  14405  dvdsrtr  14408  issubrg  14529  unitrrg  14576  aprnzr  14599  opprdrng  14620  islmod  14627  islmodd  14629  lmodfopne  14663  lmodprop2d  14685  lssvacl  14702  lssvsubcl  14703  lssvscl  14712  islss3  14716  lsslss  14718  lss1d  14720  lsspropdg  14768  dflidl2rng  14818  expghmap  14942  mulgghm2  14943  znval  14971  znunit  14994  znrrg  14995  assapropd  15014  assamulgscmlem1  15041  assamulgscmlem2  15042  psrbaglesuppg  15057  mplvalcoe  15081  neissex  15266  tgrest  15270  ssrest  15283  restopn2  15284  cnco  15322  cnss1  15327  cnss2  15328  cnptopresti  15339  uptx  15375  txrest  15377  psmetres2  15434  xmetres2  15480  xblss2ps  15505  blhalf  15509  blssexps  15530  blssex  15531  blin2  15533  blbas  15534  bdmetval  15601  metcnpi  15616  metcnpi2  15617  qtopbas  15623  tgqioo  15656  cncfss  15684  mulc1cncf  15690  cncfmptid  15698  dedekindicc  15734  ivthdec  15745  cnplimcim  15768  cnplimclemle  15769  cnplimccntop  15771  limccnp2cntop  15778  dvfgg  15789  dvcj  15810  dvrecap  15814  dvmptfsum  15826  dveflem  15827  elply2  15836  ply1termlem  15843  plymullem1  15849  eflt  15876  ptolemy  15925  cos11  15954  rpcxpmul2  16015  cxplt  16018  cxple  16019  cxplt3  16022  apcxp2  16041  rprelogbmul  16057  rprelogbdiv  16059  birthdaylem3  16089  pellexlem3  16093  sgmval  16097  sgmval2  16098  sgmf  16100  sgmmul  16110  perfect  16115  lgsval2lem  16129  lgsdir2lem5  16151  2sqlem6  16239  umgrnloopv  16355  upgredg  16385  usgr1eop  16486  upgredginwlk  16597  wlkv0  16610  clwwlkccatlem  16641  pw1map  17025  pwtrufal  17027  nninfalllem1  17051  nninfsellemqall  17058  nnnninfex  17065  sbthom  17071  qdencn  17072  isomninnlem  17079  trirec0  17093  apdiff  17097  qdiff  17098  iswomninnlem  17099  ismkvnnlem  17102  ltlenmkv  17120