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  3126  ifnefals  3654  prneimg  3862  exmid01  4294  pwntru  4295  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  poinxp  4801  mpteqb  5746  fvmptt  5747  fcof1  5934  acexmid  6027  fsuppeqg  6426  fvn0elsupp  6429  suppssdc  6438  suppssfvg  6441  dftpos4  6472  tfrlem3ag  6518  tfrlem3a  6519  tfrlemi1  6541  tfrexlem  6543  tfr1onlem3ag  6546  nntr2  6714  dcdifsnid  6715  qsel  6824  ecopovsymg  6846  ecopoverg  6848  th3qlem1  6849  mapss  6903  xpmapenlem  7078  findcard2  7121  findcard2s  7122  findcard2sd  7124  unfiin  7161  f1finf1o  7189  fidcenumlemrk  7196  fidcenumlemr  7197  fidcenum  7198  sbthlemi6  7204  sbthlemi8  7206  elfi2  7214  supisolem  7250  enumct  7357  nninfninc  7365  ismkvnex  7397  exmidontriimlem4  7482  netap  7516  2omotaplemap  7519  cc2lem  7528  dfplpq2  7617  dfmpq2  7618  mulpipqqs  7636  distrnqg  7650  ltexnqq  7671  subhalfnqq  7677  prarloclemarch  7681  nnnq0lem1  7709  distrnq0  7722  npsspw  7734  prarloclemlo  7757  prarloclem3  7760  prarloclemcalc  7765  genplt2i  7773  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  ltprordil  7852  ltexprlemlol  7865  ltexprlemupu  7867  addextpr  7884  recexprlemopl  7888  recexprlemdisj  7893  recexprlem1ssl  7896  aptiprleml  7902  prsrlem1  8005  recexgt0sr  8036  addcnsr  8097  mulcnsr  8098  mulcnsrec  8106  axaddcl  8127  axmulcl  8129  axmulcom  8134  rereceu  8152  mpomulf  8212  ltntri  8349  cnegexlem1  8396  cnegex  8399  addsub4  8464  le2add  8666  lt2add  8667  lt2sub  8682  le2sub  8683  rereim  8808  apreim  8825  mulreim  8826  addext  8832  mulext  8836  receuap  8891  rec11ap  8932  rec11rap  8933  divdivdivap  8935  ddcanap  8948  divadddivap  8949  divsubdivap  8950  conjmulap  8951  rerecclap  8952  subrecap  9061  recgt0  9072  prodgt0gt0  9073  prodgt0  9074  prodge0  9076  ltmul12a  9082  lemul12a  9084  lemulge11  9088  lt2mul2div  9101  ltrec  9105  lerec  9106  lt2msq  9108  ltrec1  9110  le2msq  9123  msq11  9124  ledivp1  9125  mulle0r  9166  peano5uzti  9632  eluzuzle  9808  qreccl  9920  elpq  9927  xrltso  10075  z2ge  10105  xpncan  10150  xaddge0  10157  xle2add  10158  xleaddadd  10166  ixxss1  10183  ixxss2  10184  elioc2  10215  divelunit  10281  fzass4  10342  fzrev  10364  fzonmapblen  10472  elfzodifsumelfzo  10492  ssfzo12bi  10516  rebtwn2z  10560  qbtwnxr  10563  modqid  10657  modqcyc  10667  modqaddabs  10670  modqaddmod  10671  mulqaddmodid  10672  modqadd2mod  10682  modqltm1p1mod  10684  modqsubmod  10690  modqsubmodmod  10691  modqmulmod  10697  modqmulmodr  10698  modqsubdir  10701  frecuzrdgg  10724  nninfinf  10751  seq3val  10768  seqvalcd  10769  seq3feq  10788  seq3f1olemp  10823  seqfeq4g  10839  expp1  10854  expcl2lemap  10859  expnegzap  10881  expadd  10889  expmul  10892  leexp1a  10902  expnlbnd  10972  nn0ltexp2  11017  nn0opth2  11032  bcval  11057  bcval5  11071  bcpasc  11074  hashunsng  11117  seq3coll  11152  iswrdiz  11169  sswrd  11171  ccatalpha  11239  ccatw2s1p1g  11271  swrdwrdsymbg  11294  swrdsb0eq  11295  ccatswrd  11300  pfxf  11312  pfxwrdsymbg  11320  wrd2ind  11353  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  shftfvalg  11441  shftfval  11444  seq3shft  11461  caucvgrelemrec  11602  resqrexlemdecn  11635  sqrtmul  11658  sqrtdiv  11665  leabs  11697  absexpzap  11703  ltabs  11710  abslt  11711  absle  11712  abssubap0  11713  amgm2  11741  icodiamlt  11803  qdenre  11825  maxleim  11828  maxleastlt  11838  rexico  11844  zmaxcl  11847  minmax  11853  xrmaxleastlt  11879  xrminmax  11888  climuni  11916  cn1lem  11937  iserex  11962  iserle  11965  climserle  11968  climcau  11970  summodclem2a  12005  summodc  12007  isumss  12015  fisumss  12016  fsumadd  12030  isumadd  12055  fsum2dlemstep  12058  fsum2d  12059  fisum0diag2  12071  fsumabs  12089  isumsplit  12115  geolim  12135  geo2lim  12140  geoisum  12141  geoisumr  12142  geoisum1  12143  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodseq  12207  fprodcl2lem  12229  fprod2dlemstep  12246  fprodle  12264  fprodmodd  12265  efcvgfsum  12291  eftlcl  12312  reeftlcl  12313  tanaddap  12363  zdvdsdc  12436  dvds2ln  12448  dvdsle  12468  divconjdvds  12473  dvdsext  12479  bitsfzo  12579  gcdsupex  12591  gcdsupcl  12592  bezoutlemmain  12632  bezoutlemaz  12637  bezoutlembi  12639  bezout  12645  gcdmultiplez  12655  dvdsmulgcd  12659  bezoutr  12666  bezoutr1  12667  lcmval  12698  lcmcllem  12702  ncoprmgcdne1b  12724  cncongr1  12738  isprm5  12777  prmdvdsexp  12783  sqrt2irr  12797  pw2dvdslemn  12800  pw2dvdseu  12803  nonsq  12842  powm2modprm  12888  pcmul  12937  pcqmul  12939  pcexp  12945  pcneg  12961  pcdvdstr  12963  pcprmpw2  12969  pcfac  12986  expnprm  12989  prmpwdvds  12991  mul4sq  13030  ssnnctlemct  13130  infpn2  13140  isstruct2r  13156  setsfun  13180  setsfun0  13181  ismndd  13583  submnd0  13590  mhmf1o  13616  resmhm  13633  mhmco  13636  mhmima  13637  dfgrp2  13673  grprcan  13683  grplmulf1o  13720  grplactcnv  13748  pwssub  13759  mhmmnd  13766  mulgval  13772  mulgz  13800  mulgnn0dir  13802  mulgdir  13804  mulgneg2  13806  mhmmulg  13813  issubg4m  13843  nmzsubg  13860  ssnmz  13861  ghmmhmb  13904  resghm  13910  ghmpreima  13916  ghmnsgpreima  13919  ghmf1o  13925  eqgabl  13980  gsumfzconst  13991  rngpropd  14032  srglmhm  14070  srgrmhm  14071  isring  14077  ringadd2  14104  ringpropd  14115  ringlghm  14138  ringrghm  14139  oppr1g  14159  dvdsrex  14176  dvdsrtr  14179  issubrg  14299  unitrrg  14346  islmod  14370  islmodd  14372  lmodfopne  14405  lmodprop2d  14427  lssvacl  14444  lssvsubcl  14445  lssvscl  14454  islss3  14458  lsslss  14460  lss1d  14462  lsspropdg  14510  dflidl2rng  14560  gsumfzfsumlemm  14666  expghmap  14686  mulgghm2  14687  znval  14715  znunit  14738  znrrg  14739  psrbaglesuppg  14751  mplvalcoe  14774  neissex  14959  tgrest  14963  ssrest  14976  restopn2  14977  cnco  15015  cnss1  15020  cnss2  15021  cnptopresti  15032  uptx  15068  txrest  15070  psmetres2  15127  xmetres2  15173  xblss2ps  15198  blhalf  15202  blssexps  15223  blssex  15224  blin2  15226  blbas  15227  bdmetval  15294  metcnpi  15309  metcnpi2  15310  qtopbas  15316  tgqioo  15349  cncfss  15377  mulc1cncf  15383  cncfmptid  15391  dedekindicc  15427  ivthdec  15438  cnplimcim  15461  cnplimclemle  15462  cnplimccntop  15464  limccnp2cntop  15471  dvfgg  15482  dvcj  15503  dvrecap  15507  dvmptfsum  15519  dveflem  15520  elply2  15529  ply1termlem  15536  plymullem1  15542  eflt  15569  ptolemy  15618  cos11  15647  rpcxpmul2  15707  cxplt  15710  cxple  15711  cxplt3  15714  apcxp2  15733  rprelogbmul  15749  rprelogbdiv  15751  pellexlem3  15776  sgmval  15780  sgmval2  15781  sgmf  15783  sgmmul  15793  perfect  15798  lgsval2lem  15812  lgsdir2lem5  15834  2sqlem6  15922  umgrnloopv  16038  upgredg  16068  usgr1eop  16169  upgredginwlk  16280  wlkv0  16293  clwwlkccatlem  16324  2omap  16698  pw1map  16700  pwtrufal  16702  nninfalllem1  16717  nninfsellemqall  16724  nnnninfex  16731  sbthom  16737  qdencn  16738  isomninnlem  16745  trirec0  16759  apdiff  16763  qdiff  16764  iswomninnlem  16765  ismkvnnlem  16768  ltlenmkv  16786