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  3852  exmid01  4282  pwntru  4283  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  poinxp  4788  mpteqb  5727  fvmptt  5728  fcof1  5913  acexmid  6006  dftpos4  6415  tfrlem3ag  6461  tfrlem3a  6462  tfrlemi1  6484  tfrexlem  6486  tfr1onlem3ag  6489  nntr2  6657  dcdifsnid  6658  qsel  6767  ecopovsymg  6789  ecopoverg  6791  th3qlem1  6792  mapss  6846  xpmapenlem  7018  findcard2  7059  findcard2s  7060  findcard2sd  7062  unfiin  7099  f1finf1o  7125  fidcenumlemrk  7132  fidcenumlemr  7133  fidcenum  7134  sbthlemi6  7140  sbthlemi8  7142  elfi2  7150  supisolem  7186  enumct  7293  nninfninc  7301  ismkvnex  7333  exmidontriimlem4  7417  netap  7451  2omotaplemap  7454  cc2lem  7463  dfplpq2  7552  dfmpq2  7553  mulpipqqs  7571  distrnqg  7585  ltexnqq  7606  subhalfnqq  7612  prarloclemarch  7616  nnnq0lem1  7644  distrnq0  7657  npsspw  7669  prarloclemlo  7692  prarloclem3  7695  prarloclemcalc  7700  genplt2i  7708  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  ltprordil  7787  ltexprlemlol  7800  ltexprlemupu  7802  addextpr  7819  recexprlemopl  7823  recexprlemdisj  7828  recexprlem1ssl  7831  aptiprleml  7837  prsrlem1  7940  recexgt0sr  7971  addcnsr  8032  mulcnsr  8033  mulcnsrec  8041  axaddcl  8062  axmulcl  8064  axmulcom  8069  rereceu  8087  mpomulf  8147  ltntri  8285  cnegexlem1  8332  cnegex  8335  addsub4  8400  le2add  8602  lt2add  8603  lt2sub  8618  le2sub  8619  rereim  8744  apreim  8761  mulreim  8762  addext  8768  mulext  8772  receuap  8827  rec11ap  8868  rec11rap  8869  divdivdivap  8871  ddcanap  8884  divadddivap  8885  divsubdivap  8886  conjmulap  8887  rerecclap  8888  subrecap  8997  recgt0  9008  prodgt0gt0  9009  prodgt0  9010  prodge0  9012  ltmul12a  9018  lemul12a  9020  lemulge11  9024  lt2mul2div  9037  ltrec  9041  lerec  9042  lt2msq  9044  ltrec1  9046  le2msq  9059  msq11  9060  ledivp1  9061  mulle0r  9102  peano5uzti  9566  eluzuzle  9742  qreccl  9849  elpq  9856  xrltso  10004  z2ge  10034  xpncan  10079  xaddge0  10086  xle2add  10087  xleaddadd  10095  ixxss1  10112  ixxss2  10113  elioc2  10144  divelunit  10210  fzass4  10270  fzrev  10292  fzonmapblen  10399  elfzodifsumelfzo  10419  ssfzo12bi  10443  rebtwn2z  10486  qbtwnxr  10489  modqid  10583  modqcyc  10593  modqaddabs  10596  modqaddmod  10597  mulqaddmodid  10598  modqadd2mod  10608  modqltm1p1mod  10610  modqsubmod  10616  modqsubmodmod  10617  modqmulmod  10623  modqmulmodr  10624  modqsubdir  10627  frecuzrdgg  10650  nninfinf  10677  seq3val  10694  seqvalcd  10695  seq3feq  10714  seq3f1olemp  10749  seqfeq4g  10765  expp1  10780  expcl2lemap  10785  expnegzap  10807  expadd  10815  expmul  10818  leexp1a  10828  expnlbnd  10898  nn0ltexp2  10943  nn0opth2  10958  bcval  10983  bcval5  10997  bcpasc  11000  hashunsng  11042  seq3coll  11077  iswrdiz  11091  sswrd  11093  ccatalpha  11161  swrdwrdsymbg  11211  swrdsb0eq  11212  ccatswrd  11217  pfxf  11229  pfxwrdsymbg  11237  wrd2ind  11270  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  shftfvalg  11344  shftfval  11347  seq3shft  11364  caucvgrelemrec  11505  resqrexlemdecn  11538  sqrtmul  11561  sqrtdiv  11568  leabs  11600  absexpzap  11606  ltabs  11613  abslt  11614  absle  11615  abssubap0  11616  amgm2  11644  icodiamlt  11706  qdenre  11728  maxleim  11731  maxleastlt  11741  rexico  11747  zmaxcl  11750  minmax  11756  xrmaxleastlt  11782  xrminmax  11791  climuni  11819  cn1lem  11840  iserex  11865  iserle  11868  climserle  11871  climcau  11873  summodclem2a  11907  summodc  11909  isumss  11917  fisumss  11918  fsumadd  11932  isumadd  11957  fsum2dlemstep  11960  fsum2d  11961  fisum0diag2  11973  fsumabs  11991  isumsplit  12017  geolim  12037  geo2lim  12042  geoisum  12043  geoisumr  12044  geoisum1  12045  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodseq  12109  fprodcl2lem  12131  fprod2dlemstep  12148  fprodle  12166  fprodmodd  12167  efcvgfsum  12193  eftlcl  12214  reeftlcl  12215  tanaddap  12265  zdvdsdc  12338  dvds2ln  12350  dvdsle  12370  divconjdvds  12375  dvdsext  12381  bitsfzo  12481  gcdsupex  12493  gcdsupcl  12494  bezoutlemmain  12534  bezoutlemaz  12539  bezoutlembi  12541  bezout  12547  gcdmultiplez  12557  dvdsmulgcd  12561  bezoutr  12568  bezoutr1  12569  lcmval  12600  lcmcllem  12604  ncoprmgcdne1b  12626  cncongr1  12640  isprm5  12679  prmdvdsexp  12685  sqrt2irr  12699  pw2dvdslemn  12702  pw2dvdseu  12705  nonsq  12744  powm2modprm  12790  pcmul  12839  pcqmul  12841  pcexp  12847  pcneg  12863  pcdvdstr  12865  pcprmpw2  12871  pcfac  12888  expnprm  12891  prmpwdvds  12893  mul4sq  12932  ssnnctlemct  13032  infpn2  13042  isstruct2r  13058  setsfun  13082  setsfun0  13083  ismndd  13485  submnd0  13492  mhmf1o  13518  resmhm  13535  mhmco  13538  mhmima  13539  dfgrp2  13575  grprcan  13585  grplmulf1o  13622  grplactcnv  13650  pwssub  13661  mhmmnd  13668  mulgval  13674  mulgz  13702  mulgnn0dir  13704  mulgdir  13706  mulgneg2  13708  mhmmulg  13715  issubg4m  13745  nmzsubg  13762  ssnmz  13763  ghmmhmb  13806  resghm  13812  ghmpreima  13818  ghmnsgpreima  13821  ghmf1o  13827  eqgabl  13882  gsumfzconst  13893  rngpropd  13933  srglmhm  13971  srgrmhm  13972  isring  13978  ringadd2  14005  ringpropd  14016  ringlghm  14039  ringrghm  14040  oppr1g  14060  dvdsrex  14077  dvdsrtr  14080  issubrg  14200  unitrrg  14246  islmod  14270  islmodd  14272  lmodfopne  14305  lmodprop2d  14327  lssvacl  14344  lssvsubcl  14345  lssvscl  14354  islss3  14358  lsslss  14360  lss1d  14362  lsspropdg  14410  dflidl2rng  14460  gsumfzfsumlemm  14566  expghmap  14586  mulgghm2  14587  znval  14615  znunit  14638  znrrg  14639  psrbaglesuppg  14651  mplvalcoe  14669  neissex  14854  tgrest  14858  ssrest  14871  restopn2  14872  cnco  14910  cnss1  14915  cnss2  14916  cnptopresti  14927  uptx  14963  txrest  14965  psmetres2  15022  xmetres2  15068  xblss2ps  15093  blhalf  15097  blssexps  15118  blssex  15119  blin2  15121  blbas  15122  bdmetval  15189  metcnpi  15204  metcnpi2  15205  qtopbas  15211  tgqioo  15244  cncfss  15272  mulc1cncf  15278  cncfmptid  15286  dedekindicc  15322  ivthdec  15333  cnplimcim  15356  cnplimclemle  15357  cnplimccntop  15359  limccnp2cntop  15366  dvfgg  15377  dvcj  15398  dvrecap  15402  dvmptfsum  15414  dveflem  15415  elply2  15424  ply1termlem  15431  plymullem1  15437  eflt  15464  ptolemy  15513  cos11  15542  rpcxpmul2  15602  cxplt  15605  cxple  15606  cxplt3  15609  apcxp2  15628  rprelogbmul  15644  rprelogbdiv  15646  sgmval  15672  sgmval2  15673  sgmf  15675  sgmmul  15685  perfect  15690  lgsval2lem  15704  lgsdir2lem5  15726  2sqlem6  15814  umgrnloopv  15929  upgredg  15957  upgredginwlk  16097  wlkv0  16110  clwwlkccatlem  16137  2omap  16418  pw1map  16420  pwtrufal  16422  nninfalllem1  16434  nninfsellemqall  16441  nnnninfex  16448  sbthom  16454  qdencn  16455  isomninnlem  16458  trirec0  16472  apdiff  16476  iswomninnlem  16477  ismkvnnlem  16480  ltlenmkv  16498