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  1060  simp2ll  1064  simp3ll  1068  rmob  3057  prneimg  3776  exmid01  4200  pwntru  4201  ordtri2or2exmidlem  4527  onsucelsucexmidlem  4530  poinxp  4697  mpteqb  5609  fvmptt  5610  fcof1  5787  acexmid  5877  dftpos4  6267  tfrlem3ag  6313  tfrlem3a  6314  tfrlemi1  6336  tfrexlem  6338  tfr1onlem3ag  6341  nntr2  6507  dcdifsnid  6508  qsel  6615  ecopovsymg  6637  ecopoverg  6639  th3qlem1  6640  mapss  6694  xpmapenlem  6852  findcard2  6892  findcard2s  6893  findcard2sd  6895  unfiin  6928  f1finf1o  6949  fidcenumlemrk  6956  fidcenumlemr  6957  fidcenum  6958  sbthlemi6  6964  sbthlemi8  6966  elfi2  6974  supisolem  7010  enumct  7117  ismkvnex  7156  exmidontriimlem4  7226  netap  7256  2omotaplemap  7259  cc2lem  7268  dfplpq2  7356  dfmpq2  7357  mulpipqqs  7375  distrnqg  7389  ltexnqq  7410  subhalfnqq  7416  prarloclemarch  7420  nnnq0lem1  7448  distrnq0  7461  npsspw  7473  prarloclemlo  7496  prarloclem3  7499  prarloclemcalc  7504  genplt2i  7512  distrlem1prl  7584  distrlem1pru  7585  distrlem4prl  7586  distrlem4pru  7587  ltprordil  7591  ltexprlemlol  7604  ltexprlemupu  7606  addextpr  7623  recexprlemopl  7627  recexprlemdisj  7632  recexprlem1ssl  7635  aptiprleml  7641  prsrlem1  7744  recexgt0sr  7775  addcnsr  7836  mulcnsr  7837  mulcnsrec  7845  axaddcl  7866  axmulcl  7868  axmulcom  7873  rereceu  7891  ltntri  8088  cnegexlem1  8135  cnegex  8138  addsub4  8203  le2add  8404  lt2add  8405  lt2sub  8420  le2sub  8421  rereim  8546  apreim  8563  mulreim  8564  addext  8570  mulext  8574  receuap  8629  rec11ap  8670  rec11rap  8671  divdivdivap  8673  ddcanap  8686  divadddivap  8687  divsubdivap  8688  conjmulap  8689  rerecclap  8690  subrecap  8799  recgt0  8810  prodgt0gt0  8811  prodgt0  8812  prodge0  8814  ltmul12a  8820  lemul12a  8822  lemulge11  8826  lt2mul2div  8839  ltrec  8843  lerec  8844  lt2msq  8846  ltrec1  8848  le2msq  8861  msq11  8862  ledivp1  8863  mulle0r  8904  peano5uzti  9364  eluzuzle  9539  qreccl  9645  elpq  9651  xrltso  9799  z2ge  9829  xpncan  9874  xaddge0  9881  xle2add  9882  xleaddadd  9890  ixxss1  9907  ixxss2  9908  elioc2  9939  divelunit  10005  fzass4  10065  fzrev  10087  fzonmapblen  10190  elfzodifsumelfzo  10204  ssfzo12bi  10228  rebtwn2z  10258  qbtwnxr  10261  modqid  10352  modqcyc  10362  modqaddabs  10365  modqaddmod  10366  mulqaddmodid  10367  modqadd2mod  10377  modqltm1p1mod  10379  modqsubmod  10385  modqsubmodmod  10386  modqmulmod  10392  modqmulmodr  10393  modqsubdir  10396  frecuzrdgg  10419  seq3val  10461  seqvalcd  10462  seq3feq  10475  seq3f1olemp  10505  expp1  10530  expcl2lemap  10535  expnegzap  10557  expadd  10565  expmul  10568  leexp1a  10578  expnlbnd  10648  nn0ltexp2  10692  nn0opth2  10707  bcval  10732  bcval5  10746  bcpasc  10749  hashunsng  10790  seq3coll  10825  shftfvalg  10830  shftfval  10833  seq3shft  10850  caucvgrelemrec  10991  resqrexlemdecn  11024  sqrtmul  11047  sqrtdiv  11054  leabs  11086  absexpzap  11092  ltabs  11099  abslt  11100  absle  11101  abssubap0  11102  amgm2  11130  icodiamlt  11192  qdenre  11214  maxleim  11217  maxleastlt  11227  rexico  11233  zmaxcl  11236  minmax  11241  xrmaxleastlt  11267  xrminmax  11276  climuni  11304  cn1lem  11325  iserex  11350  iserle  11353  climserle  11356  climcau  11358  summodclem2a  11392  summodc  11394  isumss  11402  fisumss  11403  fsumadd  11417  isumadd  11442  fsum2dlemstep  11445  fsum2d  11446  fisum0diag2  11458  fsumabs  11476  isumsplit  11502  geolim  11522  geo2lim  11527  geoisum  11528  geoisumr  11529  geoisum1  11530  mertenslemub  11545  mertenslemi1  11546  mertenslem2  11547  mertensabs  11548  prodmodclem2  11588  prodmodc  11589  zproddc  11590  fprodseq  11594  fprodcl2lem  11616  fprod2dlemstep  11633  fprodle  11651  fprodmodd  11652  efcvgfsum  11678  eftlcl  11699  reeftlcl  11700  tanaddap  11750  zdvdsdc  11822  dvds2ln  11834  dvdsle  11853  divconjdvds  11858  dvdsext  11864  gcdsupex  11961  gcdsupcl  11962  bezoutlemmain  12002  bezoutlemaz  12007  bezoutlembi  12009  bezout  12015  gcdmultiplez  12025  dvdsmulgcd  12029  bezoutr  12036  bezoutr1  12037  lcmval  12066  lcmcllem  12070  ncoprmgcdne1b  12092  cncongr1  12106  isprm5  12145  prmdvdsexp  12151  sqrt2irr  12165  pw2dvdslemn  12168  pw2dvdseu  12171  nonsq  12210  powm2modprm  12255  pcmul  12304  pcqmul  12306  pcexp  12312  pcneg  12327  pcdvdstr  12329  pcprmpw2  12335  pcfac  12351  expnprm  12354  prmpwdvds  12356  mul4sq  12395  ssnnctlemct  12450  infpn2  12460  isstruct2r  12476  setsfun  12500  setsfun0  12501  ismndd  12844  submnd0  12851  mhmf1o  12867  mhmco  12880  mhmima  12881  dfgrp2  12908  grprcan  12916  grplmulf1o  12950  grplactcnv  12978  mhmmnd  12986  mulgval  12992  mulgz  13017  mulgnn0dir  13019  mulgdir  13021  mulgneg2  13023  mhmmulg  13030  issubg4m  13059  nmzsubg  13076  ssnmz  13077  srglmhm  13182  srgrmhm  13183  isring  13189  ringadd2  13216  ringpropd  13223  oppr1g  13258  dvdsrex  13273  dvdsrtr  13276  issubrg  13348  islmod  13387  islmodd  13389  lmodfopne  13422  lmodprop2d  13444  lssvacl  13458  lssvsubcl  13459  lssvscl  13468  islss3  13472  lsslss  13474  lss1d  13476  lsspropdg  13523  neissex  13805  tgrest  13809  ssrest  13822  restopn2  13823  cnco  13861  cnss1  13866  cnss2  13867  cnptopresti  13878  uptx  13914  txrest  13916  psmetres2  13973  xmetres2  14019  xblss2ps  14044  blhalf  14048  blssexps  14069  blssex  14070  blin2  14072  blbas  14073  bdmetval  14140  metcnpi  14155  metcnpi2  14156  qtopbas  14162  tgqioo  14187  cncfss  14210  mulc1cncf  14216  cncfmptid  14223  dedekindicc  14251  ivthdec  14262  cnplimcim  14276  cnplimclemle  14277  cnplimccntop  14279  limccnp2cntop  14286  dvfgg  14297  dvcj  14313  dvrecap  14317  dveflem  14327  eflt  14336  ptolemy  14385  cos11  14414  cxplt  14476  cxple  14477  cxplt3  14480  apcxp2  14498  rprelogbmul  14513  rprelogbdiv  14515  lgsval2lem  14551  lgsdir2lem5  14573  2sqlem6  14607  pwtrufal  14888  nninfalllem1  14898  nninfsellemqall  14905  sbthom  14915  qdencn  14916  isomninnlem  14919  trirec0  14933  apdiff  14937  iswomninnlem  14938  ismkvnnlem  14941  ltlenmkv  14959