Theorem simpll 518

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 479	1 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1ll  1044  simp2ll  1048  simp3ll  1052  rmob  3001  prneimg  3701  exmid01  4121  pwntru  4122  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  poinxp  4608  mpteqb  5511  fvmptt  5512  fcof1  5684  acexmid  5773  grprinvlem  5965  dftpos4  6160  tfrlem3ag  6206  tfrlem3a  6207  tfrlemi1  6229  tfrexlem  6231  tfr1onlem3ag  6234  nntr2  6399  dcdifsnid  6400  qsel  6506  ecopovsymg  6528  ecopoverg  6530  th3qlem1  6531  mapss  6585  xpmapenlem  6743  findcard2  6783  findcard2s  6784  findcard2sd  6786  unfiin  6814  f1finf1o  6835  fidcenumlemrk  6842  fidcenumlemr  6843  fidcenum  6844  sbthlemi6  6850  sbthlemi8  6852  elfi2  6860  supisolem  6895  enumct  7000  ismkvnex  7029  dfplpq2  7162  dfmpq2  7163  mulpipqqs  7181  distrnqg  7195  ltexnqq  7216  subhalfnqq  7222  prarloclemarch  7226  nnnq0lem1  7254  distrnq0  7267  npsspw  7279  prarloclemlo  7302  prarloclem3  7305  prarloclemcalc  7310  genplt2i  7318  distrlem1prl  7390  distrlem1pru  7391  distrlem4prl  7392  distrlem4pru  7393  ltprordil  7397  ltexprlemlol  7410  ltexprlemupu  7412  addextpr  7429  recexprlemopl  7433  recexprlemdisj  7438  recexprlem1ssl  7441  aptiprleml  7447  prsrlem1  7550  recexgt0sr  7581  addcnsr  7642  mulcnsr  7643  mulcnsrec  7651  axaddcl  7672  axmulcl  7674  axmulcom  7679  rereceu  7697  ltntri  7890  cnegexlem1  7937  cnegex  7940  addsub4  8005  le2add  8206  lt2add  8207  lt2sub  8222  le2sub  8223  rereim  8348  apreim  8365  mulreim  8366  addext  8372  mulext  8376  receuap  8430  rec11ap  8470  rec11rap  8471  divdivdivap  8473  ddcanap  8486  divadddivap  8487  divsubdivap  8488  conjmulap  8489  rerecclap  8490  subrecap  8598  recgt0  8608  prodgt0gt0  8609  prodgt0  8610  prodge0  8612  ltmul12a  8618  lemul12a  8620  lemulge11  8624  lt2mul2div  8637  ltrec  8641  lerec  8642  lt2msq  8644  ltrec1  8646  le2msq  8659  msq11  8660  ledivp1  8661  mulle0r  8702  peano5uzti  9159  eluzuzle  9334  qreccl  9434  xrltso  9582  z2ge  9609  xpncan  9654  xaddge0  9661  xle2add  9662  xleaddadd  9670  ixxss1  9687  ixxss2  9688  elioc2  9719  divelunit  9785  fzass4  9842  fzrev  9864  fzonmapblen  9964  elfzodifsumelfzo  9978  ssfzo12bi  10002  rebtwn2z  10032  qbtwnxr  10035  modqid  10122  modqcyc  10132  modqaddabs  10135  modqaddmod  10136  mulqaddmodid  10137  modqadd2mod  10147  modqltm1p1mod  10149  modqsubmod  10155  modqsubmodmod  10156  modqmulmod  10162  modqmulmodr  10163  modqsubdir  10166  frecuzrdgg  10189  seq3val  10231  seqvalcd  10232  seq3feq  10245  seq3f1olemp  10275  expp1  10300  expcl2lemap  10305  expnegzap  10327  expadd  10335  expmul  10338  leexp1a  10348  expnlbnd  10416  nn0opth2  10470  bcval  10495  bcval5  10509  bcpasc  10512  hashunsng  10553  seq3coll  10585  shftfvalg  10590  shftfval  10593  seq3shft  10610  caucvgrelemrec  10751  resqrexlemdecn  10784  sqrtmul  10807  sqrtdiv  10814  leabs  10846  absexpzap  10852  ltabs  10859  abslt  10860  absle  10861  abssubap0  10862  amgm2  10890  icodiamlt  10952  qdenre  10974  maxleim  10977  maxleastlt  10987  rexico  10993  zmaxcl  10996  minmax  11001  xrmaxleastlt  11025  xrminmax  11034  climuni  11062  cn1lem  11083  iserex  11108  iserle  11111  climserle  11114  climcau  11116  summodclem2a  11150  summodc  11152  isumss  11160  fisumss  11161  fsumadd  11175  isumadd  11200  fsum2dlemstep  11203  fsum2d  11204  fisum0diag2  11216  fsumabs  11234  isumsplit  11260  geolim  11280  geo2lim  11285  geoisum  11286  geoisumr  11287  geoisum1  11288  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodmodclem2  11346  prodmodc  11347  efcvgfsum  11373  eftlcl  11394  reeftlcl  11395  tanaddap  11446  zdvdsdc  11514  dvds2ln  11526  dvdsle  11542  divconjdvds  11547  dvdsext  11553  gcdsupex  11646  gcdsupcl  11647  bezoutlemmain  11686  bezoutlemaz  11691  bezoutlembi  11693  bezout  11699  gcdmultiplez  11709  dvdsmulgcd  11713  bezoutr  11720  bezoutr1  11721  lcmval  11744  lcmcllem  11748  ncoprmgcdne1b  11770  cncongr1  11784  prmdvdsexp  11826  sqrt2irr  11840  pw2dvdslemn  11843  pw2dvdseu  11846  nonsq  11885  isstruct2r  11970  setsfun  11994  setsfun0  11995  neissex  12334  tgrest  12338  ssrest  12351  restopn2  12352  cnco  12390  cnss1  12395  cnss2  12396  cnptopresti  12407  uptx  12443  txrest  12445  psmetres2  12502  xmetres2  12548  xblss2ps  12573  blhalf  12577  blssexps  12598  blssex  12599  blin2  12601  blbas  12602  bdmetval  12669  metcnpi  12684  metcnpi2  12685  qtopbas  12691  tgqioo  12716  cncfss  12739  mulc1cncf  12745  cncfmptid  12752  dedekindicc  12780  ivthdec  12791  cnplimcim  12805  cnplimclemle  12806  cnplimccntop  12808  limccnp2cntop  12815  dvfgg  12826  dvcj  12842  dvrecap  12846  dveflem  12855  ptolemy  12905  pwtrufal  13192  nninfalllem1  13203  nninfsellemqall  13211  sbthom  13221  qdencn  13222  isomninnlem  13225