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  8455  cnegexlem1  8502  cnegex  8505  addsub4  8570  le2add  8773  lt2add  8774  lt2sub  8789  le2sub  8790  rereim  8916  apreim  8933  mulreim  8934  addext  8940  mulext  8944  receuap  9001  rec11ap  9042  rec11rap  9043  divdivdivap  9045  ddcanap  9058  divadddivap  9059  divsubdivap  9060  conjmulap  9061  rerecclap  9062  subrecap  9171  recgt0  9182  prodgt0gt0  9183  prodgt0  9184  prodge0  9186  ltmul12a  9192  lemul12a  9194  lemulge11  9198  lt2mul2div  9211  ltrec  9215  lerec  9216  lt2msq  9218  ltrec1  9220  le2msq  9233  msq11  9234  ledivp1  9235  mulle0r  9276  peano5uzti  9758  eluzuzle  9939  qreccl  10051  irraddap  10056  elpq  10059  xrltso  10208  z2ge  10238  xpncan  10283  xaddge0  10290  xle2add  10291  xleaddadd  10299  ixxss1  10316  ixxss2  10317  elioc2  10348  divelunit  10414  fzass4  10478  fzrev  10501  fzonmapblen  10609  elfzodifsumelfzo  10629  ssfzo12bi  10653  rebtwn2z  10699  qbtwnxr  10702  modqid  10799  modqcyc  10809  modqaddabs  10812  modqaddmod  10813  mulqaddmodid  10814  modqadd2mod  10824  modqltm1p1mod  10826  modqsubmod  10832  modqsubmodmod  10833  modqmulmod  10839  modqmulmodr  10840  modqsubdir  10843  frecuzrdgg  10866  nninfinf  10893  seq3val  10910  seqvalcd  10911  seq3feq  10930  seq3f1olemp  10965  seqfeq4g  10981  expp1  10996  expcl2lemap  11001  expnegzap  11023  expadd  11031  expmul  11034  leexp1a  11044  resq01  11108  expnlbnd  11115  nn0ltexp2  11161  nn0opth2  11176  bcval  11201  bcval5  11215  bcpasc  11218  hashunsng  11262  sseqn  11293  hashfibclem  11296  hashfibc  11297  hashf1lem2  11300  seq3coll  11308  iswrdiz  11325  sswrd  11327  ccatalpha  11395  ccatw2s1p1g  11427  swrdwrdsymbg  11450  swrdsb0eq  11451  ccatswrd  11456  pfxf  11468  pfxwrdsymbg  11476  wrd2ind  11509  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  shftfvalg  11597  shftfval  11600  seq3shft  11617  caucvgrelemrec  11759  resqrexlemdecn  11792  sqrtmul  11815  sqrtdiv  11822  leabs  11854  absexpzap  11861  ltabs  11868  abslt  11869  absle  11870  abssubap0  11871  amgm2  11899  icodiamlt  11961  qdenre  11983  maxleim  11986  maxleastlt  11996  rexico  12002  zmaxcl  12005  minmax  12011  zmincl  12020  xrmaxleastlt  12038  xrminmax  12047  climuni  12075  cn1lem  12096  iserex  12121  iserle  12124  climserle  12127  climcau  12129  summodclem2a  12164  summodc  12166  isumss  12174  fisumss  12175  fsumadd  12189  isumadd  12214  fsum2dlemstep  12217  fsum2d  12218  fisum0diag2  12230  fsumabs  12248  isumsplit  12274  geolim  12294  geo2lim  12299  geoisum  12300  geoisumr  12301  geoisum1  12302  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodcl2lem  12388  fprod2dlemstep  12405  fprodle  12423  fprodmodd  12424  efcvgfsum  12450  eftlcl  12471  reeftlcl  12472  tanaddap  12522  zdvdsdc  12595  dvds2ln  12607  dvdsle  12627  divconjdvds  12632  dvdsext  12638  bitsfzo  12738  gcdsupex  12750  gcdsupcl  12751  bezoutlemmain  12791  bezoutlemaz  12796  bezoutlembi  12798  bezout  12804  gcdmultiplez  12814  dvdsmulgcd  12818  bezoutr  12825  bezoutr1  12826  lcmval  12857  lcmcllem  12861  ncoprmgcdne1b  12883  cncongr1  12897  isprm5  12937  prmdvdsexp  12943  sqrt2irr  12957  pwbdvdslemn  12960  nonsq  13003  powm2modprm  13051  pcmul  13100  pcqmul  13102  pcexp  13108  pcneg  13124  pcdvdstr  13126  pcprmpw2  13132  pcfac  13149  expnprm  13152  prmpwdvds  13154  mul4sq  13193  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemsima  13308  ssnnctlemct  13386  infpn2  13396  isstruct2r  13412  setsfun  13436  setsfun0  13437  ismndd  13799  submnd0  13806  mhmf1o  13826  resmhm  13843  mhmco  13846  mhmima  13847  dfgrp2  13881  grprcan  13891  grplmulf1o  13928  grplactcnv  13956  mhmmnd  13968  mulgval  13974  mulgz  14002  mulgnn0dir  14004  mulgdir  14006  mulgneg2  14008  mhmmulg  14015  issubg4m  14045  nmzsubg  14062  ssnmz  14063  ghmmhmb  14106  resghm  14112  ghmpreima  14118  ghmnsgpreima  14121  ghmf1o  14127  eqgabl  14183  gzsumconst  14192  pwssub  14265  rngpropd  14303  srglmhm  14346  srgrmhm  14347  isring  14353  ringadd2  14381  ringpropd  14392  ringlghm  14415  ringrghm  14416  oppr1g  14437  dvdsrex  14454  dvdsrtr  14457  issubrg  14578  unitrrg  14625  aprnzr  14648  opprdrng  14669  islmod  14676  islmodd  14678  lmodfopne  14712  lmodprop2d  14734  lssvacl  14751  lssvsubcl  14752  lssvscl  14761  islss3  14765  lsslss  14767  lss1d  14769  lsspropdg  14817  dflidl2rng  14867  expghmap  14991  mulgghm2  14992  znval  15020  znunit  15043  znrrg  15044  assapropd  15063  assamulgscmlem1  15090  assamulgscmlem2  15091  psrbaglesuppg  15106  mplvalcoe  15130  neissex  15315  tgrest  15319  ssrest  15332  restopn2  15333  cnco  15371  cnss1  15376  cnss2  15377  cnptopresti  15388  uptx  15424  txrest  15426  psmetres2  15483  xmetres2  15529  xblss2ps  15554  blhalf  15558  blssexps  15579  blssex  15580  blin2  15582  blbas  15583  bdmetval  15650  metcnpi  15665  metcnpi2  15666  qtopbas  15672  tgqioo  15705  cncfss  15733  mulc1cncf  15739  cncfmptid  15747  dedekindicc  15783  ivthdec  15794  cnplimcim  15817  cnplimclemle  15818  cnplimccntop  15820  limccnp2cntop  15827  dvfgg  15838  dvcj  15859  dvrecap  15863  dvmptfsum  15875  dveflem  15876  elply2  15885  ply1termlem  15892  plymullem1  15898  eflt  15925  ptolemy  15975  cos11  16004  logdivlt  16046  logdivle  16047  rpcxpmul2  16068  cxplt  16071  cxple  16072  cxplt3  16075  apcxp2  16094  rprelogbmul  16110  rprelogbdiv  16112  birthdaylem3  16146  pellexlem3  16150  sgmval  16164  sgmval2  16165  sgmf  16167  sgmmul  16191  perfect  16199  bcmax  16203  bposlem1  16209  lgsval2lem  16227  lgsdir2lem5  16249  2sqlem6  16337  umgrnloopv  16453  upgredg  16483  usgr1eop  16584  upgredginwlk  16695  wlkv0  16708  clwwlkccatlem  16739  pw1map  17123  pwtrufal  17125  nninfalllem1  17149  nninfsellemqall  17156  nnnninfex  17163  sbthom  17169  qdencn  17170  isomninnlem  17177  trirec0  17191  apdiff  17195  qdiff  17196  iswomninnlem  17197  ismkvnnlem  17200  ltlenmkv  17218