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  1084  simp2ll  1088  simp3ll  1092  rmob  3122  ifnefals  3647  prneimg  3851  exmid01  4281  pwntru  4282  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  poinxp  4787  mpteqb  5724  fvmptt  5725  fcof1  5906  acexmid  5999  dftpos4  6407  tfrlem3ag  6453  tfrlem3a  6454  tfrlemi1  6476  tfrexlem  6478  tfr1onlem3ag  6481  nntr2  6647  dcdifsnid  6648  qsel  6757  ecopovsymg  6779  ecopoverg  6781  th3qlem1  6782  mapss  6836  xpmapenlem  7006  findcard2  7047  findcard2s  7048  findcard2sd  7050  unfiin  7084  f1finf1o  7110  fidcenumlemrk  7117  fidcenumlemr  7118  fidcenum  7119  sbthlemi6  7125  sbthlemi8  7127  elfi2  7135  supisolem  7171  enumct  7278  nninfninc  7286  ismkvnex  7318  exmidontriimlem4  7402  netap  7436  2omotaplemap  7439  cc2lem  7448  dfplpq2  7537  dfmpq2  7538  mulpipqqs  7556  distrnqg  7570  ltexnqq  7591  subhalfnqq  7597  prarloclemarch  7601  nnnq0lem1  7629  distrnq0  7642  npsspw  7654  prarloclemlo  7677  prarloclem3  7680  prarloclemcalc  7685  genplt2i  7693  distrlem1prl  7765  distrlem1pru  7766  distrlem4prl  7767  distrlem4pru  7768  ltprordil  7772  ltexprlemlol  7785  ltexprlemupu  7787  addextpr  7804  recexprlemopl  7808  recexprlemdisj  7813  recexprlem1ssl  7816  aptiprleml  7822  prsrlem1  7925  recexgt0sr  7956  addcnsr  8017  mulcnsr  8018  mulcnsrec  8026  axaddcl  8047  axmulcl  8049  axmulcom  8054  rereceu  8072  mpomulf  8132  ltntri  8270  cnegexlem1  8317  cnegex  8320  addsub4  8385  le2add  8587  lt2add  8588  lt2sub  8603  le2sub  8604  rereim  8729  apreim  8746  mulreim  8747  addext  8753  mulext  8757  receuap  8812  rec11ap  8853  rec11rap  8854  divdivdivap  8856  ddcanap  8869  divadddivap  8870  divsubdivap  8871  conjmulap  8872  rerecclap  8873  subrecap  8982  recgt0  8993  prodgt0gt0  8994  prodgt0  8995  prodge0  8997  ltmul12a  9003  lemul12a  9005  lemulge11  9009  lt2mul2div  9022  ltrec  9026  lerec  9027  lt2msq  9029  ltrec1  9031  le2msq  9044  msq11  9045  ledivp1  9046  mulle0r  9087  peano5uzti  9551  eluzuzle  9726  qreccl  9833  elpq  9840  xrltso  9988  z2ge  10018  xpncan  10063  xaddge0  10070  xle2add  10071  xleaddadd  10079  ixxss1  10096  ixxss2  10097  elioc2  10128  divelunit  10194  fzass4  10254  fzrev  10276  fzonmapblen  10383  elfzodifsumelfzo  10402  ssfzo12bi  10426  rebtwn2z  10469  qbtwnxr  10472  modqid  10566  modqcyc  10576  modqaddabs  10579  modqaddmod  10580  mulqaddmodid  10581  modqadd2mod  10591  modqltm1p1mod  10593  modqsubmod  10599  modqsubmodmod  10600  modqmulmod  10606  modqmulmodr  10607  modqsubdir  10610  frecuzrdgg  10633  nninfinf  10660  seq3val  10677  seqvalcd  10678  seq3feq  10697  seq3f1olemp  10732  seqfeq4g  10748  expp1  10763  expcl2lemap  10768  expnegzap  10790  expadd  10798  expmul  10801  leexp1a  10811  expnlbnd  10881  nn0ltexp2  10926  nn0opth2  10941  bcval  10966  bcval5  10980  bcpasc  10983  hashunsng  11024  seq3coll  11059  iswrdiz  11073  sswrd  11075  swrdwrdsymbg  11191  swrdsb0eq  11192  ccatswrd  11197  pfxf  11209  pfxwrdsymbg  11217  wrd2ind  11250  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  shftfvalg  11324  shftfval  11327  seq3shft  11344  caucvgrelemrec  11485  resqrexlemdecn  11518  sqrtmul  11541  sqrtdiv  11548  leabs  11580  absexpzap  11586  ltabs  11593  abslt  11594  absle  11595  abssubap0  11596  amgm2  11624  icodiamlt  11686  qdenre  11708  maxleim  11711  maxleastlt  11721  rexico  11727  zmaxcl  11730  minmax  11736  xrmaxleastlt  11762  xrminmax  11771  climuni  11799  cn1lem  11820  iserex  11845  iserle  11848  climserle  11851  climcau  11853  summodclem2a  11887  summodc  11889  isumss  11897  fisumss  11898  fsumadd  11912  isumadd  11937  fsum2dlemstep  11940  fsum2d  11941  fisum0diag2  11953  fsumabs  11971  isumsplit  11997  geolim  12017  geo2lim  12022  geoisum  12023  geoisumr  12024  geoisum1  12025  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodseq  12089  fprodcl2lem  12111  fprod2dlemstep  12128  fprodle  12146  fprodmodd  12147  efcvgfsum  12173  eftlcl  12194  reeftlcl  12195  tanaddap  12245  zdvdsdc  12318  dvds2ln  12330  dvdsle  12350  divconjdvds  12355  dvdsext  12361  bitsfzo  12461  gcdsupex  12473  gcdsupcl  12474  bezoutlemmain  12514  bezoutlemaz  12519  bezoutlembi  12521  bezout  12527  gcdmultiplez  12537  dvdsmulgcd  12541  bezoutr  12548  bezoutr1  12549  lcmval  12580  lcmcllem  12584  ncoprmgcdne1b  12606  cncongr1  12620  isprm5  12659  prmdvdsexp  12665  sqrt2irr  12679  pw2dvdslemn  12682  pw2dvdseu  12685  nonsq  12724  powm2modprm  12770  pcmul  12819  pcqmul  12821  pcexp  12827  pcneg  12843  pcdvdstr  12845  pcprmpw2  12851  pcfac  12868  expnprm  12871  prmpwdvds  12873  mul4sq  12912  ssnnctlemct  13012  infpn2  13022  isstruct2r  13038  setsfun  13062  setsfun0  13063  ismndd  13465  submnd0  13472  mhmf1o  13498  resmhm  13515  mhmco  13518  mhmima  13519  dfgrp2  13555  grprcan  13565  grplmulf1o  13602  grplactcnv  13630  pwssub  13641  mhmmnd  13648  mulgval  13654  mulgz  13682  mulgnn0dir  13684  mulgdir  13686  mulgneg2  13688  mhmmulg  13695  issubg4m  13725  nmzsubg  13742  ssnmz  13743  ghmmhmb  13786  resghm  13792  ghmpreima  13798  ghmnsgpreima  13801  ghmf1o  13807  eqgabl  13862  gsumfzconst  13873  rngpropd  13913  srglmhm  13951  srgrmhm  13952  isring  13958  ringadd2  13985  ringpropd  13996  ringlghm  14019  ringrghm  14020  oppr1g  14040  dvdsrex  14056  dvdsrtr  14059  issubrg  14179  unitrrg  14225  islmod  14249  islmodd  14251  lmodfopne  14284  lmodprop2d  14306  lssvacl  14323  lssvsubcl  14324  lssvscl  14333  islss3  14337  lsslss  14339  lss1d  14341  lsspropdg  14389  dflidl2rng  14439  gsumfzfsumlemm  14545  expghmap  14565  mulgghm2  14566  znval  14594  znunit  14617  znrrg  14618  psrbaglesuppg  14630  mplvalcoe  14648  neissex  14833  tgrest  14837  ssrest  14850  restopn2  14851  cnco  14889  cnss1  14894  cnss2  14895  cnptopresti  14906  uptx  14942  txrest  14944  psmetres2  15001  xmetres2  15047  xblss2ps  15072  blhalf  15076  blssexps  15097  blssex  15098  blin2  15100  blbas  15101  bdmetval  15168  metcnpi  15183  metcnpi2  15184  qtopbas  15190  tgqioo  15223  cncfss  15251  mulc1cncf  15257  cncfmptid  15265  dedekindicc  15301  ivthdec  15312  cnplimcim  15335  cnplimclemle  15336  cnplimccntop  15338  limccnp2cntop  15345  dvfgg  15356  dvcj  15377  dvrecap  15381  dvmptfsum  15393  dveflem  15394  elply2  15403  ply1termlem  15410  plymullem1  15416  eflt  15443  ptolemy  15492  cos11  15521  rpcxpmul2  15581  cxplt  15584  cxple  15585  cxplt3  15588  apcxp2  15607  rprelogbmul  15623  rprelogbdiv  15625  sgmval  15651  sgmval2  15652  sgmf  15654  sgmmul  15664  perfect  15669  lgsval2lem  15683  lgsdir2lem5  15705  2sqlem6  15793  umgrnloopv  15908  upgredg  15936  2omap  16318  pw1map  16320  pwtrufal  16322  nninfalllem1  16333  nninfsellemqall  16340  nnnninfex  16347  sbthom  16353  qdencn  16354  isomninnlem  16357  trirec0  16371  apdiff  16375  iswomninnlem  16376  ismkvnnlem  16379  ltlenmkv  16397