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  6538  tfrlem3ag  6584  tfrlem3a  6585  tfrlemi1  6607  tfrexlem  6609  tfr1onlem3ag  6612  nntr2  6780  dcdifsnid  6781  qsel  6890  ecopovsymg  6912  ecopoverg  6914  th3qlem1  6915  mapss  6977  xpmapenlem  7153  findcard2  7197  findcard2s  7198  findcard2sd  7200  unfiin  7237  f1finf1o  7269  fidcenumlemrk  7276  fidcenumlemr  7277  fidcenum  7278  sbthlemi6  7284  sbthlemi8  7286  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  9765  eluzuzle  9946  qreccl  10058  irraddap  10063  elpq  10066  xrltso  10215  z2ge  10245  xpncan  10290  xaddge0  10297  xle2add  10298  xleaddadd  10306  ixxss1  10323  ixxss2  10324  elioc2  10355  divelunit  10421  fzass4  10485  fzrev  10508  fzonmapblen  10616  elfzodifsumelfzo  10636  ssfzo12bi  10660  rebtwn2z  10706  qbtwnxr  10709  flaplt  10739  modqid  10807  modqcyc  10817  modqaddabs  10820  modqaddmod  10821  mulqaddmodid  10822  modqadd2mod  10832  modqltm1p1mod  10834  modqsubmod  10840  modqsubmodmod  10841  modqmulmod  10847  modqmulmodr  10848  modqsubdir  10851  frecuzrdgg  10874  nninfinf  10901  seq3val  10918  seqvalcd  10919  seq3feq  10938  seq3f1olemp  10973  seqfeq4g  10989  expp1  11004  expcl2lemap  11009  expnegzap  11031  expadd  11039  expmul  11042  leexp1a  11052  resq01  11116  expnlbnd  11123  nn0ltexp2  11169  nn0opth2  11184  bcval  11209  bcval5  11223  bcpasc  11226  hashunsng  11270  sseqn  11301  hashfibclem  11304  hashfibc  11305  hashf1lem2  11308  seq3coll  11316  iswrdiz  11333  sswrd  11335  ccatalpha  11403  ccatw2s1p1g  11435  swrdwrdsymbg  11458  swrdsb0eq  11459  ccatswrd  11464  pfxf  11476  pfxwrdsymbg  11484  wrd2ind  11517  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  shftfvalg  11605  shftfval  11608  seq3shft  11625  caucvgrelemrec  11767  resqrexlemdecn  11800  sqrtmul  11823  sqrtdiv  11830  leabs  11862  absexpzap  11869  ltabs  11876  abslt  11877  absle  11878  abssubap0  11879  amgm2  11907  icodiamlt  11969  qdenre  11991  maxleim  11994  maxleastlt  12004  rexico  12010  zmaxcl  12013  minmax  12020  zmincl  12029  xrmaxleastlt  12047  xrminmax  12056  climuni  12084  cn1lem  12105  iserex  12130  iserle  12133  climserle  12136  climcau  12138  summodclem2a  12173  summodc  12175  isumss  12183  fisumss  12184  fsumadd  12198  isumadd  12223  fsum2dlemstep  12226  fsum2d  12227  fisum0diag2  12239  fsumabs  12257  isumsplit  12283  geolim  12303  geo2lim  12308  geoisum  12309  geoisumr  12310  geoisum1  12311  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodcl2lem  12397  fprod2dlemstep  12414  fprodle  12432  fprodmodd  12433  efcvgfsum  12459  eftlcl  12480  reeftlcl  12481  tanaddap  12531  zdvdsdc  12604  dvds2ln  12616  dvdsle  12636  divconjdvds  12641  dvdsext  12647  bitsfzo  12747  gcdsupex  12759  gcdsupcl  12760  bezoutlemmain  12800  bezoutlemaz  12805  bezoutlembi  12807  bezout  12813  gcdmultiplez  12823  dvdsmulgcd  12827  bezoutr  12834  bezoutr1  12835  lcmval  12866  lcmcllem  12870  ncoprmgcdne1b  12892  cncongr1  12906  isprm5  12946  prmdvdsexp  12952  sqrt2irr  12966  pwbdvdslemn  12969  nonsq  13012  powm2modprm  13060  pcmul  13109  pcqmul  13111  pcexp  13117  pcneg  13133  pcdvdstr  13135  pcprmpw2  13141  pcfac  13158  expnprm  13161  prmpwdvds  13163  mul4sq  13202  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsima  13317  ssnnctlemct  13395  infpn2  13405  isstruct2r  13421  setsfun  13445  setsfun0  13446  ismndd  13809  submnd0  13816  mhmf1o  13836  resmhm  13853  mhmco  13856  mhmima  13857  dfgrp2  13891  grprcan  13901  grplmulf1o  13938  grplactcnv  13966  mhmmnd  13978  mulgval  13984  mulgz  14012  mulgnn0dir  14014  mulgdir  14016  mulgneg2  14018  mhmmulg  14025  issubg4m  14055  nmzsubg  14072  ssnmz  14073  ghmmhmb  14116  resghm  14122  ghmpreima  14128  ghmnsgpreima  14131  ghmf1o  14137  resscntz  14166  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  cntzmhm  14173  eqgabl  14224  gzsumconst  14233  gsumsnfdcmn  14257  pwssub  14323  rngpropd  14361  srglmhm  14404  srgrmhm  14405  isring  14411  ringadd2  14439  ringpropd  14450  ringlghm  14473  ringrghm  14474  oppr1g  14497  dvdsrex  14514  dvdsrtr  14517  issubrg  14638  unitrrg  14685  aprnzr  14708  opprdrng  14729  islmod  14736  islmodd  14738  lmodfopne  14772  lmodprop2d  14794  lssvacl  14811  lssvsubcl  14812  lssvscl  14821  islss3  14825  lsslss  14827  lss1d  14829  lsspropdg  14877  dflidl2rng  14927  expghmap  15051  mulgghm2  15052  znval  15080  znunit  15103  znrrg  15104  assapropd  15123  assamulgscmlem1  15150  assamulgscmlem2  15151  psrbaglesuppg  15166  mplvalcoe  15206  neissex  15391  tgrest  15395  ssrest  15408  restopn2  15409  cnco  15447  cnss1  15452  cnss2  15453  cnptopresti  15464  uptx  15500  txrest  15502  psmetres2  15559  xmetres2  15605  xblss2ps  15630  blhalf  15634  blssexps  15655  blssex  15656  blin2  15658  blbas  15659  bdmetval  15726  metcnpi  15741  metcnpi2  15742  qtopbas  15748  tgqioo  15781  cncfss  15809  mulc1cncf  15815  cncfmptid  15823  dedekindicc  15859  ivthdec  15870  cnplimcim  15893  cnplimclemle  15894  cnplimccntop  15896  limccnp2cntop  15903  dvfgg  15914  dvcj  15935  dvrecap  15939  dvmptfsum  15951  dveflem  15952  elply2  15961  ply1termlem  15968  plymullem1  15974  eflt  16001  ptolemy  16051  cos11  16081  logdivlt  16124  logdivle  16125  rpcxpmul2  16146  rpcxpmul2z  16148  cxplt  16151  cxple  16152  cxplt3  16155  apcxp2  16174  rprelogbmul  16191  rprelogbdiv  16193  birthdaylem3  16227  pellexlem3  16231  efnnfsumcl  16239  sgmval  16252  sgmval2  16253  sgmf  16255  efchtqdvds  16265  sgmmul  16290  perfect  16301  bcmax  16305  bposlem1  16311  bpos  16320  lgsval2lem  16334  lgsdir2lem5  16356  2sqlem6  16444  umgrnloopv  16560  upgredg  16590  usgr1eop  16691  upgredginwlk  16802  wlkv0  16815  clwwlkccatlem  16846  pw1map  17230  pwtrufal  17232  nninfalllem1  17257  nninfsellemqall  17264  nnnninfex  17271  sbthom  17277  qdencn  17278  isomninnlem  17285  trirec0  17300  apdiff  17304  qdiff  17305  iswomninnlem  17306  ismkvnnlem  17309  ltlenmkv  17327