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  1063  simp2ll  1067  simp3ll  1071  rmob  3095  ifnefals  3619  prneimg  3821  exmid01  4250  pwntru  4251  ordtri2or2exmidlem  4582  onsucelsucexmidlem  4585  poinxp  4752  mpteqb  5683  fvmptt  5684  fcof1  5865  acexmid  5956  dftpos4  6362  tfrlem3ag  6408  tfrlem3a  6409  tfrlemi1  6431  tfrexlem  6433  tfr1onlem3ag  6436  nntr2  6602  dcdifsnid  6603  qsel  6712  ecopovsymg  6734  ecopoverg  6736  th3qlem1  6737  mapss  6791  xpmapenlem  6961  findcard2  7001  findcard2s  7002  findcard2sd  7004  unfiin  7038  f1finf1o  7064  fidcenumlemrk  7071  fidcenumlemr  7072  fidcenum  7073  sbthlemi6  7079  sbthlemi8  7081  elfi2  7089  supisolem  7125  enumct  7232  nninfninc  7240  ismkvnex  7272  exmidontriimlem4  7352  netap  7386  2omotaplemap  7389  cc2lem  7398  dfplpq2  7487  dfmpq2  7488  mulpipqqs  7506  distrnqg  7520  ltexnqq  7541  subhalfnqq  7547  prarloclemarch  7551  nnnq0lem1  7579  distrnq0  7592  npsspw  7604  prarloclemlo  7627  prarloclem3  7630  prarloclemcalc  7635  genplt2i  7643  distrlem1prl  7715  distrlem1pru  7716  distrlem4prl  7717  distrlem4pru  7718  ltprordil  7722  ltexprlemlol  7735  ltexprlemupu  7737  addextpr  7754  recexprlemopl  7758  recexprlemdisj  7763  recexprlem1ssl  7766  aptiprleml  7772  prsrlem1  7875  recexgt0sr  7906  addcnsr  7967  mulcnsr  7968  mulcnsrec  7976  axaddcl  7997  axmulcl  7999  axmulcom  8004  rereceu  8022  mpomulf  8082  ltntri  8220  cnegexlem1  8267  cnegex  8270  addsub4  8335  le2add  8537  lt2add  8538  lt2sub  8553  le2sub  8554  rereim  8679  apreim  8696  mulreim  8697  addext  8703  mulext  8707  receuap  8762  rec11ap  8803  rec11rap  8804  divdivdivap  8806  ddcanap  8819  divadddivap  8820  divsubdivap  8821  conjmulap  8822  rerecclap  8823  subrecap  8932  recgt0  8943  prodgt0gt0  8944  prodgt0  8945  prodge0  8947  ltmul12a  8953  lemul12a  8955  lemulge11  8959  lt2mul2div  8972  ltrec  8976  lerec  8977  lt2msq  8979  ltrec1  8981  le2msq  8994  msq11  8995  ledivp1  8996  mulle0r  9037  peano5uzti  9501  eluzuzle  9676  qreccl  9783  elpq  9790  xrltso  9938  z2ge  9968  xpncan  10013  xaddge0  10020  xle2add  10021  xleaddadd  10029  ixxss1  10046  ixxss2  10047  elioc2  10078  divelunit  10144  fzass4  10204  fzrev  10226  fzonmapblen  10333  elfzodifsumelfzo  10352  ssfzo12bi  10376  rebtwn2z  10419  qbtwnxr  10422  modqid  10516  modqcyc  10526  modqaddabs  10529  modqaddmod  10530  mulqaddmodid  10531  modqadd2mod  10541  modqltm1p1mod  10543  modqsubmod  10549  modqsubmodmod  10550  modqmulmod  10556  modqmulmodr  10557  modqsubdir  10560  frecuzrdgg  10583  nninfinf  10610  seq3val  10627  seqvalcd  10628  seq3feq  10647  seq3f1olemp  10682  seqfeq4g  10698  expp1  10713  expcl2lemap  10718  expnegzap  10740  expadd  10748  expmul  10751  leexp1a  10761  expnlbnd  10831  nn0ltexp2  10876  nn0opth2  10891  bcval  10916  bcval5  10930  bcpasc  10933  hashunsng  10974  seq3coll  11009  iswrdiz  11023  sswrd  11025  swrdwrdsymbg  11140  swrdsb0eq  11141  ccatswrd  11146  pfxf  11158  pfxwrdsymbg  11166  wrd2ind  11199  shftfvalg  11204  shftfval  11207  seq3shft  11224  caucvgrelemrec  11365  resqrexlemdecn  11398  sqrtmul  11421  sqrtdiv  11428  leabs  11460  absexpzap  11466  ltabs  11473  abslt  11474  absle  11475  abssubap0  11476  amgm2  11504  icodiamlt  11566  qdenre  11588  maxleim  11591  maxleastlt  11601  rexico  11607  zmaxcl  11610  minmax  11616  xrmaxleastlt  11642  xrminmax  11651  climuni  11679  cn1lem  11700  iserex  11725  iserle  11728  climserle  11731  climcau  11733  summodclem2a  11767  summodc  11769  isumss  11777  fisumss  11778  fsumadd  11792  isumadd  11817  fsum2dlemstep  11820  fsum2d  11821  fisum0diag2  11833  fsumabs  11851  isumsplit  11877  geolim  11897  geo2lim  11902  geoisum  11903  geoisumr  11904  geoisum1  11905  mertenslemub  11920  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  prodmodclem2  11963  prodmodc  11964  zproddc  11965  fprodseq  11969  fprodcl2lem  11991  fprod2dlemstep  12008  fprodle  12026  fprodmodd  12027  efcvgfsum  12053  eftlcl  12074  reeftlcl  12075  tanaddap  12125  zdvdsdc  12198  dvds2ln  12210  dvdsle  12230  divconjdvds  12235  dvdsext  12241  bitsfzo  12341  gcdsupex  12353  gcdsupcl  12354  bezoutlemmain  12394  bezoutlemaz  12399  bezoutlembi  12401  bezout  12407  gcdmultiplez  12417  dvdsmulgcd  12421  bezoutr  12428  bezoutr1  12429  lcmval  12460  lcmcllem  12464  ncoprmgcdne1b  12486  cncongr1  12500  isprm5  12539  prmdvdsexp  12545  sqrt2irr  12559  pw2dvdslemn  12562  pw2dvdseu  12565  nonsq  12604  powm2modprm  12650  pcmul  12699  pcqmul  12701  pcexp  12707  pcneg  12723  pcdvdstr  12725  pcprmpw2  12731  pcfac  12748  expnprm  12751  prmpwdvds  12753  mul4sq  12792  ssnnctlemct  12892  infpn2  12902  isstruct2r  12918  setsfun  12942  setsfun0  12943  ismndd  13344  submnd0  13351  mhmf1o  13377  resmhm  13394  mhmco  13397  mhmima  13398  dfgrp2  13434  grprcan  13444  grplmulf1o  13481  grplactcnv  13509  pwssub  13520  mhmmnd  13527  mulgval  13533  mulgz  13561  mulgnn0dir  13563  mulgdir  13565  mulgneg2  13567  mhmmulg  13574  issubg4m  13604  nmzsubg  13621  ssnmz  13622  ghmmhmb  13665  resghm  13671  ghmpreima  13677  ghmnsgpreima  13680  ghmf1o  13686  eqgabl  13741  gsumfzconst  13752  rngpropd  13792  srglmhm  13830  srgrmhm  13831  isring  13837  ringadd2  13864  ringpropd  13875  ringlghm  13898  ringrghm  13899  oppr1g  13919  dvdsrex  13935  dvdsrtr  13938  issubrg  14058  unitrrg  14104  islmod  14128  islmodd  14130  lmodfopne  14163  lmodprop2d  14185  lssvacl  14202  lssvsubcl  14203  lssvscl  14212  islss3  14216  lsslss  14218  lss1d  14220  lsspropdg  14268  dflidl2rng  14318  gsumfzfsumlemm  14424  expghmap  14444  mulgghm2  14445  znval  14473  znunit  14496  znrrg  14497  psrbaglesuppg  14509  mplvalcoe  14527  neissex  14712  tgrest  14716  ssrest  14729  restopn2  14730  cnco  14768  cnss1  14773  cnss2  14774  cnptopresti  14785  uptx  14821  txrest  14823  psmetres2  14880  xmetres2  14926  xblss2ps  14951  blhalf  14955  blssexps  14976  blssex  14977  blin2  14979  blbas  14980  bdmetval  15047  metcnpi  15062  metcnpi2  15063  qtopbas  15069  tgqioo  15102  cncfss  15130  mulc1cncf  15136  cncfmptid  15144  dedekindicc  15180  ivthdec  15191  cnplimcim  15214  cnplimclemle  15215  cnplimccntop  15217  limccnp2cntop  15224  dvfgg  15235  dvcj  15256  dvrecap  15260  dvmptfsum  15272  dveflem  15273  elply2  15282  ply1termlem  15289  plymullem1  15295  eflt  15322  ptolemy  15371  cos11  15400  rpcxpmul2  15460  cxplt  15463  cxple  15464  cxplt3  15467  apcxp2  15486  rprelogbmul  15502  rprelogbdiv  15504  sgmval  15530  sgmval2  15531  sgmf  15533  sgmmul  15543  perfect  15548  lgsval2lem  15562  lgsdir2lem5  15584  2sqlem6  15672  umgrnloopvv  15785  2omap  16071  pw1map  16073  pwtrufal  16075  nninfalllem1  16086  nninfsellemqall  16093  nnnninfex  16100  sbthom  16106  qdencn  16107  isomninnlem  16110  trirec0  16124  apdiff  16128  iswomninnlem  16129  ismkvnnlem  16132  ltlenmkv  16150