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  1086  simp2ll  1090  simp3ll  1094  rmob  3125  ifnefals  3650  prneimg  3857  exmid01  4288  pwntru  4289  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  poinxp  4795  mpteqb  5737  fvmptt  5738  fcof1  5923  acexmid  6016  dftpos4  6428  tfrlem3ag  6474  tfrlem3a  6475  tfrlemi1  6497  tfrexlem  6499  tfr1onlem3ag  6502  nntr2  6670  dcdifsnid  6671  qsel  6780  ecopovsymg  6802  ecopoverg  6804  th3qlem1  6805  mapss  6859  xpmapenlem  7034  findcard2  7077  findcard2s  7078  findcard2sd  7080  unfiin  7117  f1finf1o  7145  fidcenumlemrk  7152  fidcenumlemr  7153  fidcenum  7154  sbthlemi6  7160  sbthlemi8  7162  elfi2  7170  supisolem  7206  enumct  7313  nninfninc  7321  ismkvnex  7353  exmidontriimlem4  7438  netap  7472  2omotaplemap  7475  cc2lem  7484  dfplpq2  7573  dfmpq2  7574  mulpipqqs  7592  distrnqg  7606  ltexnqq  7627  subhalfnqq  7633  prarloclemarch  7637  nnnq0lem1  7665  distrnq0  7678  npsspw  7690  prarloclemlo  7713  prarloclem3  7716  prarloclemcalc  7721  genplt2i  7729  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  ltprordil  7808  ltexprlemlol  7821  ltexprlemupu  7823  addextpr  7840  recexprlemopl  7844  recexprlemdisj  7849  recexprlem1ssl  7852  aptiprleml  7858  prsrlem1  7961  recexgt0sr  7992  addcnsr  8053  mulcnsr  8054  mulcnsrec  8062  axaddcl  8083  axmulcl  8085  axmulcom  8090  rereceu  8108  mpomulf  8168  ltntri  8306  cnegexlem1  8353  cnegex  8356  addsub4  8421  le2add  8623  lt2add  8624  lt2sub  8639  le2sub  8640  rereim  8765  apreim  8782  mulreim  8783  addext  8789  mulext  8793  receuap  8848  rec11ap  8889  rec11rap  8890  divdivdivap  8892  ddcanap  8905  divadddivap  8906  divsubdivap  8907  conjmulap  8908  rerecclap  8909  subrecap  9018  recgt0  9029  prodgt0gt0  9030  prodgt0  9031  prodge0  9033  ltmul12a  9039  lemul12a  9041  lemulge11  9045  lt2mul2div  9058  ltrec  9062  lerec  9063  lt2msq  9065  ltrec1  9067  le2msq  9080  msq11  9081  ledivp1  9082  mulle0r  9123  peano5uzti  9587  eluzuzle  9763  qreccl  9875  elpq  9882  xrltso  10030  z2ge  10060  xpncan  10105  xaddge0  10112  xle2add  10113  xleaddadd  10121  ixxss1  10138  ixxss2  10139  elioc2  10170  divelunit  10236  fzass4  10296  fzrev  10318  fzonmapblen  10425  elfzodifsumelfzo  10445  ssfzo12bi  10469  rebtwn2z  10513  qbtwnxr  10516  modqid  10610  modqcyc  10620  modqaddabs  10623  modqaddmod  10624  mulqaddmodid  10625  modqadd2mod  10635  modqltm1p1mod  10637  modqsubmod  10643  modqsubmodmod  10644  modqmulmod  10650  modqmulmodr  10651  modqsubdir  10654  frecuzrdgg  10677  nninfinf  10704  seq3val  10721  seqvalcd  10722  seq3feq  10741  seq3f1olemp  10776  seqfeq4g  10792  expp1  10807  expcl2lemap  10812  expnegzap  10834  expadd  10842  expmul  10845  leexp1a  10855  expnlbnd  10925  nn0ltexp2  10970  nn0opth2  10985  bcval  11010  bcval5  11024  bcpasc  11027  hashunsng  11070  seq3coll  11105  iswrdiz  11119  sswrd  11121  ccatalpha  11189  ccatw2s1p1g  11221  swrdwrdsymbg  11244  swrdsb0eq  11245  ccatswrd  11250  pfxf  11262  pfxwrdsymbg  11270  wrd2ind  11303  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  shftfvalg  11378  shftfval  11381  seq3shft  11398  caucvgrelemrec  11539  resqrexlemdecn  11572  sqrtmul  11595  sqrtdiv  11602  leabs  11634  absexpzap  11640  ltabs  11647  abslt  11648  absle  11649  abssubap0  11650  amgm2  11678  icodiamlt  11740  qdenre  11762  maxleim  11765  maxleastlt  11775  rexico  11781  zmaxcl  11784  minmax  11790  xrmaxleastlt  11816  xrminmax  11825  climuni  11853  cn1lem  11874  iserex  11899  iserle  11902  climserle  11905  climcau  11907  summodclem2a  11941  summodc  11943  isumss  11951  fisumss  11952  fsumadd  11966  isumadd  11991  fsum2dlemstep  11994  fsum2d  11995  fisum0diag2  12007  fsumabs  12025  isumsplit  12051  geolim  12071  geo2lim  12076  geoisum  12077  geoisumr  12078  geoisum1  12079  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodcl2lem  12165  fprod2dlemstep  12182  fprodle  12200  fprodmodd  12201  efcvgfsum  12227  eftlcl  12248  reeftlcl  12249  tanaddap  12299  zdvdsdc  12372  dvds2ln  12384  dvdsle  12404  divconjdvds  12409  dvdsext  12415  bitsfzo  12515  gcdsupex  12527  gcdsupcl  12528  bezoutlemmain  12568  bezoutlemaz  12573  bezoutlembi  12575  bezout  12581  gcdmultiplez  12591  dvdsmulgcd  12595  bezoutr  12602  bezoutr1  12603  lcmval  12634  lcmcllem  12638  ncoprmgcdne1b  12660  cncongr1  12674  isprm5  12713  prmdvdsexp  12719  sqrt2irr  12733  pw2dvdslemn  12736  pw2dvdseu  12739  nonsq  12778  powm2modprm  12824  pcmul  12873  pcqmul  12875  pcexp  12881  pcneg  12897  pcdvdstr  12899  pcprmpw2  12905  pcfac  12922  expnprm  12925  prmpwdvds  12927  mul4sq  12966  ssnnctlemct  13066  infpn2  13076  isstruct2r  13092  setsfun  13116  setsfun0  13117  ismndd  13519  submnd0  13526  mhmf1o  13552  resmhm  13569  mhmco  13572  mhmima  13573  dfgrp2  13609  grprcan  13619  grplmulf1o  13656  grplactcnv  13684  pwssub  13695  mhmmnd  13702  mulgval  13708  mulgz  13736  mulgnn0dir  13738  mulgdir  13740  mulgneg2  13742  mhmmulg  13749  issubg4m  13779  nmzsubg  13796  ssnmz  13797  ghmmhmb  13840  resghm  13846  ghmpreima  13852  ghmnsgpreima  13855  ghmf1o  13861  eqgabl  13916  gsumfzconst  13927  rngpropd  13967  srglmhm  14005  srgrmhm  14006  isring  14012  ringadd2  14039  ringpropd  14050  ringlghm  14073  ringrghm  14074  oppr1g  14094  dvdsrex  14111  dvdsrtr  14114  issubrg  14234  unitrrg  14280  islmod  14304  islmodd  14306  lmodfopne  14339  lmodprop2d  14361  lssvacl  14378  lssvsubcl  14379  lssvscl  14388  islss3  14392  lsslss  14394  lss1d  14396  lsspropdg  14444  dflidl2rng  14494  gsumfzfsumlemm  14600  expghmap  14620  mulgghm2  14621  znval  14649  znunit  14672  znrrg  14673  psrbaglesuppg  14685  mplvalcoe  14703  neissex  14888  tgrest  14892  ssrest  14905  restopn2  14906  cnco  14944  cnss1  14949  cnss2  14950  cnptopresti  14961  uptx  14997  txrest  14999  psmetres2  15056  xmetres2  15102  xblss2ps  15127  blhalf  15131  blssexps  15152  blssex  15153  blin2  15155  blbas  15156  bdmetval  15223  metcnpi  15238  metcnpi2  15239  qtopbas  15245  tgqioo  15278  cncfss  15306  mulc1cncf  15312  cncfmptid  15320  dedekindicc  15356  ivthdec  15367  cnplimcim  15390  cnplimclemle  15391  cnplimccntop  15393  limccnp2cntop  15400  dvfgg  15411  dvcj  15432  dvrecap  15436  dvmptfsum  15448  dveflem  15449  elply2  15458  ply1termlem  15465  plymullem1  15471  eflt  15498  ptolemy  15547  cos11  15576  rpcxpmul2  15636  cxplt  15639  cxple  15640  cxplt3  15643  apcxp2  15662  rprelogbmul  15678  rprelogbdiv  15680  sgmval  15706  sgmval2  15707  sgmf  15709  sgmmul  15719  perfect  15724  lgsval2lem  15738  lgsdir2lem5  15760  2sqlem6  15848  umgrnloopv  15964  upgredg  15994  usgr1eop  16095  upgredginwlk  16206  wlkv0  16219  clwwlkccatlem  16250  2omap  16594  pw1map  16596  pwtrufal  16598  nninfalllem1  16610  nninfsellemqall  16617  nnnninfex  16624  sbthom  16630  qdencn  16631  isomninnlem  16634  trirec0  16648  apdiff  16652  iswomninnlem  16653  ismkvnnlem  16656  ltlenmkv  16674