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  3136  ifnefals  3667  prneimg  3878  exmid01  4311  pwntru  4312  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  poinxp  4819  mpteqb  5768  fvmptt  5769  fcof1  5956  acexmid  6049  fsuppeqg  6448  fvn0elsupp  6451  suppssdc  6460  suppssfvg  6463  dftpos4  6494  tfrlem3ag  6540  tfrlem3a  6541  tfrlemi1  6563  tfrexlem  6565  tfr1onlem3ag  6568  nntr2  6736  dcdifsnid  6737  qsel  6846  ecopovsymg  6868  ecopoverg  6870  th3qlem1  6871  mapss  6926  xpmapenlem  7102  findcard2  7146  findcard2s  7147  findcard2sd  7149  unfiin  7186  f1finf1o  7217  fidcenumlemrk  7224  fidcenumlemr  7225  fidcenum  7226  sbthlemi6  7232  sbthlemi8  7234  elfi2  7259  2omap  7269  2omapfi  7271  supisolem  7299  enumct  7406  nninfninc  7414  ismkvnex  7446  exmidontriimlem4  7531  netap  7568  2omotaplemap  7571  cc2lem  7580  dfplpq2  7669  dfmpq2  7670  mulpipqqs  7688  distrnqg  7702  ltexnqq  7723  subhalfnqq  7729  prarloclemarch  7733  nnnq0lem1  7761  distrnq0  7774  npsspw  7786  prarloclemlo  7809  prarloclem3  7812  prarloclemcalc  7817  genplt2i  7825  distrlem1prl  7897  distrlem1pru  7898  distrlem4prl  7899  distrlem4pru  7900  ltprordil  7904  ltexprlemlol  7917  ltexprlemupu  7919  addextpr  7936  recexprlemopl  7940  recexprlemdisj  7945  recexprlem1ssl  7948  aptiprleml  7954  prsrlem1  8057  recexgt0sr  8088  addcnsr  8149  mulcnsr  8150  mulcnsrec  8158  axaddcl  8179  axmulcl  8181  axmulcom  8186  rereceu  8204  mpomulf  8264  ltntri  8401  cnegexlem1  8448  cnegex  8451  addsub4  8516  le2add  8718  lt2add  8719  lt2sub  8734  le2sub  8735  rereim  8860  apreim  8877  mulreim  8878  addext  8884  mulext  8888  receuap  8943  rec11ap  8984  rec11rap  8985  divdivdivap  8987  ddcanap  9000  divadddivap  9001  divsubdivap  9002  conjmulap  9003  rerecclap  9004  subrecap  9113  recgt0  9124  prodgt0gt0  9125  prodgt0  9126  prodge0  9128  ltmul12a  9134  lemul12a  9136  lemulge11  9140  lt2mul2div  9153  ltrec  9157  lerec  9158  lt2msq  9160  ltrec1  9162  le2msq  9175  msq11  9176  ledivp1  9177  mulle0r  9218  peano5uzti  9686  eluzuzle  9862  qreccl  9974  elpq  9981  xrltso  10129  z2ge  10159  xpncan  10204  xaddge0  10211  xle2add  10212  xleaddadd  10220  ixxss1  10237  ixxss2  10238  elioc2  10269  divelunit  10335  fzass4  10396  fzrev  10418  fzonmapblen  10526  elfzodifsumelfzo  10546  ssfzo12bi  10570  rebtwn2z  10614  qbtwnxr  10617  modqid  10711  modqcyc  10721  modqaddabs  10724  modqaddmod  10725  mulqaddmodid  10726  modqadd2mod  10736  modqltm1p1mod  10738  modqsubmod  10744  modqsubmodmod  10745  modqmulmod  10751  modqmulmodr  10752  modqsubdir  10755  frecuzrdgg  10778  nninfinf  10805  seq3val  10822  seqvalcd  10823  seq3feq  10842  seq3f1olemp  10877  seqfeq4g  10893  expp1  10908  expcl2lemap  10913  expnegzap  10935  expadd  10943  expmul  10946  leexp1a  10956  expnlbnd  11026  nn0ltexp2  11071  nn0opth2  11086  bcval  11111  bcval5  11125  bcpasc  11128  hashunsng  11172  sseqn  11203  hashfibclem  11206  hashfibc  11207  seq3coll  11214  iswrdiz  11231  sswrd  11233  ccatalpha  11301  ccatw2s1p1g  11333  swrdwrdsymbg  11356  swrdsb0eq  11357  ccatswrd  11362  pfxf  11374  pfxwrdsymbg  11382  wrd2ind  11415  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  shftfvalg  11503  shftfval  11506  seq3shft  11523  caucvgrelemrec  11664  resqrexlemdecn  11697  sqrtmul  11720  sqrtdiv  11727  leabs  11759  absexpzap  11765  ltabs  11772  abslt  11773  absle  11774  abssubap0  11775  amgm2  11803  icodiamlt  11865  qdenre  11887  maxleim  11890  maxleastlt  11900  rexico  11906  zmaxcl  11909  minmax  11915  xrmaxleastlt  11941  xrminmax  11950  climuni  11978  cn1lem  11999  iserex  12024  iserle  12027  climserle  12030  climcau  12032  summodclem2a  12067  summodc  12069  isumss  12077  fisumss  12078  fsumadd  12092  isumadd  12117  fsum2dlemstep  12120  fsum2d  12121  fisum0diag2  12133  fsumabs  12151  isumsplit  12177  geolim  12197  geo2lim  12202  geoisum  12203  geoisumr  12204  geoisum1  12205  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodseq  12269  fprodcl2lem  12291  fprod2dlemstep  12308  fprodle  12326  fprodmodd  12327  efcvgfsum  12353  eftlcl  12374  reeftlcl  12375  tanaddap  12425  zdvdsdc  12498  dvds2ln  12510  dvdsle  12530  divconjdvds  12535  dvdsext  12541  bitsfzo  12641  gcdsupex  12653  gcdsupcl  12654  bezoutlemmain  12694  bezoutlemaz  12699  bezoutlembi  12701  bezout  12707  gcdmultiplez  12717  dvdsmulgcd  12721  bezoutr  12728  bezoutr1  12729  lcmval  12760  lcmcllem  12764  ncoprmgcdne1b  12786  cncongr1  12800  isprm5  12839  prmdvdsexp  12845  sqrt2irr  12859  pw2dvdslemn  12862  pw2dvdseu  12865  nonsq  12904  powm2modprm  12950  pcmul  12999  pcqmul  13001  pcexp  13007  pcneg  13023  pcdvdstr  13025  pcprmpw2  13031  pcfac  13048  expnprm  13051  prmpwdvds  13053  mul4sq  13092  ballotfilem2  13142  ssnnctlemct  13197  infpn2  13207  isstruct2r  13223  setsfun  13247  setsfun0  13248  ismndd  13650  submnd0  13657  mhmf1o  13683  resmhm  13700  mhmco  13703  mhmima  13704  dfgrp2  13740  grprcan  13750  grplmulf1o  13787  grplactcnv  13815  pwssub  13826  mhmmnd  13833  mulgval  13839  mulgz  13867  mulgnn0dir  13869  mulgdir  13871  mulgneg2  13873  mhmmulg  13880  issubg4m  13910  nmzsubg  13927  ssnmz  13928  ghmmhmb  13971  resghm  13977  ghmpreima  13983  ghmnsgpreima  13986  ghmf1o  13992  eqgabl  14047  gsumfzconst  14058  rngpropd  14099  srglmhm  14137  srgrmhm  14138  isring  14144  ringadd2  14171  ringpropd  14182  ringlghm  14205  ringrghm  14206  oppr1g  14226  dvdsrex  14243  dvdsrtr  14246  issubrg  14366  unitrrg  14413  aprnzr  14433  islmod  14439  islmodd  14441  lmodfopne  14474  lmodprop2d  14496  lssvacl  14513  lssvsubcl  14514  lssvscl  14523  islss3  14527  lsslss  14529  lss1d  14531  lsspropdg  14579  dflidl2rng  14629  gsumfzfsumlemm  14735  expghmap  14755  mulgghm2  14756  znval  14784  znunit  14807  znrrg  14808  psrbaglesuppg  14821  mplvalcoe  14845  neissex  15030  tgrest  15034  ssrest  15047  restopn2  15048  cnco  15086  cnss1  15091  cnss2  15092  cnptopresti  15103  uptx  15139  txrest  15141  psmetres2  15198  xmetres2  15244  xblss2ps  15269  blhalf  15273  blssexps  15294  blssex  15295  blin2  15297  blbas  15298  bdmetval  15365  metcnpi  15380  metcnpi2  15381  qtopbas  15387  tgqioo  15420  cncfss  15448  mulc1cncf  15454  cncfmptid  15462  dedekindicc  15498  ivthdec  15509  cnplimcim  15532  cnplimclemle  15533  cnplimccntop  15535  limccnp2cntop  15542  dvfgg  15553  dvcj  15574  dvrecap  15578  dvmptfsum  15590  dveflem  15591  elply2  15600  ply1termlem  15607  plymullem1  15613  eflt  15640  ptolemy  15689  cos11  15718  rpcxpmul2  15778  cxplt  15781  cxple  15782  cxplt3  15785  apcxp2  15804  rprelogbmul  15820  rprelogbdiv  15822  pellexlem3  15847  sgmval  15851  sgmval2  15852  sgmf  15854  sgmmul  15864  perfect  15869  lgsval2lem  15883  lgsdir2lem5  15905  2sqlem6  15993  umgrnloopv  16109  upgredg  16139  usgr1eop  16240  upgredginwlk  16351  wlkv0  16364  clwwlkccatlem  16395  pw1map  16769  pwtrufal  16771  nninfalllem1  16786  nninfsellemqall  16793  nnnninfex  16800  sbthom  16806  qdencn  16807  isomninnlem  16814  trirec0  16828  apdiff  16832  qdiff  16833  iswomninnlem  16834  ismkvnnlem  16837  ltlenmkv  16856