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  3123  ifnefals  3648  prneimg  3855  exmid01  4286  pwntru  4287  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  poinxp  4793  mpteqb  5733  fvmptt  5734  fcof1  5919  acexmid  6012  dftpos4  6424  tfrlem3ag  6470  tfrlem3a  6471  tfrlemi1  6493  tfrexlem  6495  tfr1onlem3ag  6498  nntr2  6666  dcdifsnid  6667  qsel  6776  ecopovsymg  6798  ecopoverg  6800  th3qlem1  6801  mapss  6855  xpmapenlem  7030  findcard2  7071  findcard2s  7072  findcard2sd  7074  unfiin  7111  f1finf1o  7137  fidcenumlemrk  7144  fidcenumlemr  7145  fidcenum  7146  sbthlemi6  7152  sbthlemi8  7154  elfi2  7162  supisolem  7198  enumct  7305  nninfninc  7313  ismkvnex  7345  exmidontriimlem4  7429  netap  7463  2omotaplemap  7466  cc2lem  7475  dfplpq2  7564  dfmpq2  7565  mulpipqqs  7583  distrnqg  7597  ltexnqq  7618  subhalfnqq  7624  prarloclemarch  7628  nnnq0lem1  7656  distrnq0  7669  npsspw  7681  prarloclemlo  7704  prarloclem3  7707  prarloclemcalc  7712  genplt2i  7720  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  ltprordil  7799  ltexprlemlol  7812  ltexprlemupu  7814  addextpr  7831  recexprlemopl  7835  recexprlemdisj  7840  recexprlem1ssl  7843  aptiprleml  7849  prsrlem1  7952  recexgt0sr  7983  addcnsr  8044  mulcnsr  8045  mulcnsrec  8053  axaddcl  8074  axmulcl  8076  axmulcom  8081  rereceu  8099  mpomulf  8159  ltntri  8297  cnegexlem1  8344  cnegex  8347  addsub4  8412  le2add  8614  lt2add  8615  lt2sub  8630  le2sub  8631  rereim  8756  apreim  8773  mulreim  8774  addext  8780  mulext  8784  receuap  8839  rec11ap  8880  rec11rap  8881  divdivdivap  8883  ddcanap  8896  divadddivap  8897  divsubdivap  8898  conjmulap  8899  rerecclap  8900  subrecap  9009  recgt0  9020  prodgt0gt0  9021  prodgt0  9022  prodge0  9024  ltmul12a  9030  lemul12a  9032  lemulge11  9036  lt2mul2div  9049  ltrec  9053  lerec  9054  lt2msq  9056  ltrec1  9058  le2msq  9071  msq11  9072  ledivp1  9073  mulle0r  9114  peano5uzti  9578  eluzuzle  9754  qreccl  9866  elpq  9873  xrltso  10021  z2ge  10051  xpncan  10096  xaddge0  10103  xle2add  10104  xleaddadd  10112  ixxss1  10129  ixxss2  10130  elioc2  10161  divelunit  10227  fzass4  10287  fzrev  10309  fzonmapblen  10416  elfzodifsumelfzo  10436  ssfzo12bi  10460  rebtwn2z  10504  qbtwnxr  10507  modqid  10601  modqcyc  10611  modqaddabs  10614  modqaddmod  10615  mulqaddmodid  10616  modqadd2mod  10626  modqltm1p1mod  10628  modqsubmod  10634  modqsubmodmod  10635  modqmulmod  10641  modqmulmodr  10642  modqsubdir  10645  frecuzrdgg  10668  nninfinf  10695  seq3val  10712  seqvalcd  10713  seq3feq  10732  seq3f1olemp  10767  seqfeq4g  10783  expp1  10798  expcl2lemap  10803  expnegzap  10825  expadd  10833  expmul  10836  leexp1a  10846  expnlbnd  10916  nn0ltexp2  10961  nn0opth2  10976  bcval  11001  bcval5  11015  bcpasc  11018  hashunsng  11061  seq3coll  11096  iswrdiz  11110  sswrd  11112  ccatalpha  11180  ccatw2s1p1g  11212  swrdwrdsymbg  11235  swrdsb0eq  11236  ccatswrd  11241  pfxf  11253  pfxwrdsymbg  11261  wrd2ind  11294  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  shftfvalg  11369  shftfval  11372  seq3shft  11389  caucvgrelemrec  11530  resqrexlemdecn  11563  sqrtmul  11586  sqrtdiv  11593  leabs  11625  absexpzap  11631  ltabs  11638  abslt  11639  absle  11640  abssubap0  11641  amgm2  11669  icodiamlt  11731  qdenre  11753  maxleim  11756  maxleastlt  11766  rexico  11772  zmaxcl  11775  minmax  11781  xrmaxleastlt  11807  xrminmax  11816  climuni  11844  cn1lem  11865  iserex  11890  iserle  11893  climserle  11896  climcau  11898  summodclem2a  11932  summodc  11934  isumss  11942  fisumss  11943  fsumadd  11957  isumadd  11982  fsum2dlemstep  11985  fsum2d  11986  fisum0diag2  11998  fsumabs  12016  isumsplit  12042  geolim  12062  geo2lim  12067  geoisum  12068  geoisumr  12069  geoisum1  12070  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodcl2lem  12156  fprod2dlemstep  12173  fprodle  12191  fprodmodd  12192  efcvgfsum  12218  eftlcl  12239  reeftlcl  12240  tanaddap  12290  zdvdsdc  12363  dvds2ln  12375  dvdsle  12395  divconjdvds  12400  dvdsext  12406  bitsfzo  12506  gcdsupex  12518  gcdsupcl  12519  bezoutlemmain  12559  bezoutlemaz  12564  bezoutlembi  12566  bezout  12572  gcdmultiplez  12582  dvdsmulgcd  12586  bezoutr  12593  bezoutr1  12594  lcmval  12625  lcmcllem  12629  ncoprmgcdne1b  12651  cncongr1  12665  isprm5  12704  prmdvdsexp  12710  sqrt2irr  12724  pw2dvdslemn  12727  pw2dvdseu  12730  nonsq  12769  powm2modprm  12815  pcmul  12864  pcqmul  12866  pcexp  12872  pcneg  12888  pcdvdstr  12890  pcprmpw2  12896  pcfac  12913  expnprm  12916  prmpwdvds  12918  mul4sq  12957  ssnnctlemct  13057  infpn2  13067  isstruct2r  13083  setsfun  13107  setsfun0  13108  ismndd  13510  submnd0  13517  mhmf1o  13543  resmhm  13560  mhmco  13563  mhmima  13564  dfgrp2  13600  grprcan  13610  grplmulf1o  13647  grplactcnv  13675  pwssub  13686  mhmmnd  13693  mulgval  13699  mulgz  13727  mulgnn0dir  13729  mulgdir  13731  mulgneg2  13733  mhmmulg  13740  issubg4m  13770  nmzsubg  13787  ssnmz  13788  ghmmhmb  13831  resghm  13837  ghmpreima  13843  ghmnsgpreima  13846  ghmf1o  13852  eqgabl  13907  gsumfzconst  13918  rngpropd  13958  srglmhm  13996  srgrmhm  13997  isring  14003  ringadd2  14030  ringpropd  14041  ringlghm  14064  ringrghm  14065  oppr1g  14085  dvdsrex  14102  dvdsrtr  14105  issubrg  14225  unitrrg  14271  islmod  14295  islmodd  14297  lmodfopne  14330  lmodprop2d  14352  lssvacl  14369  lssvsubcl  14370  lssvscl  14379  islss3  14383  lsslss  14385  lss1d  14387  lsspropdg  14435  dflidl2rng  14485  gsumfzfsumlemm  14591  expghmap  14611  mulgghm2  14612  znval  14640  znunit  14663  znrrg  14664  psrbaglesuppg  14676  mplvalcoe  14694  neissex  14879  tgrest  14883  ssrest  14896  restopn2  14897  cnco  14935  cnss1  14940  cnss2  14941  cnptopresti  14952  uptx  14988  txrest  14990  psmetres2  15047  xmetres2  15093  xblss2ps  15118  blhalf  15122  blssexps  15143  blssex  15144  blin2  15146  blbas  15147  bdmetval  15214  metcnpi  15229  metcnpi2  15230  qtopbas  15236  tgqioo  15269  cncfss  15297  mulc1cncf  15303  cncfmptid  15311  dedekindicc  15347  ivthdec  15358  cnplimcim  15381  cnplimclemle  15382  cnplimccntop  15384  limccnp2cntop  15391  dvfgg  15402  dvcj  15423  dvrecap  15427  dvmptfsum  15439  dveflem  15440  elply2  15449  ply1termlem  15456  plymullem1  15462  eflt  15489  ptolemy  15538  cos11  15567  rpcxpmul2  15627  cxplt  15630  cxple  15631  cxplt3  15634  apcxp2  15653  rprelogbmul  15669  rprelogbdiv  15671  sgmval  15697  sgmval2  15698  sgmf  15700  sgmmul  15710  perfect  15715  lgsval2lem  15729  lgsdir2lem5  15751  2sqlem6  15839  umgrnloopv  15955  upgredg  15983  usgr1eop  16084  upgredginwlk  16153  wlkv0  16166  clwwlkccatlem  16195  2omap  16530  pw1map  16532  pwtrufal  16534  nninfalllem1  16546  nninfsellemqall  16553  nnnninfex  16560  sbthom  16566  qdencn  16567  isomninnlem  16570  trirec0  16584  apdiff  16588  iswomninnlem  16589  ismkvnnlem  16592  ltlenmkv  16610