Theorem simprd 114

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
simprd.1	|- ( ph -> ( ps /\ ch ) )

Assertion

Ref	Expression
simprd	|- ( ph -> ch )

Proof of Theorem simprd

Step	Hyp	Ref	Expression
1		simprd.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		simpr 110	. 2 |- ( ( ps /\ ch ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  biimpr  130  simprbi  275  simplbda  384  simplrd  530  simprld  532  simprrd  534  simp2  1025  simp3  1026  sbh  1825  eldifbd  3226  unssbd  3401  opth  4359  potr  4435  frind  4479  brrelex2  4797  funinsn  5411  feu  5555  fcnvres  5556  fun11iun  5641  funopsn  5866  elmpocl2  6260  uchoice  6345  oprssdmm  6379  fczsupp0  6473  tfrlem1  6553  tfrlemisucfn  6569  tfrlemisucaccv  6570  tfrlemibxssdm  6572  tfrlemibfn  6573  tfrlemi14d  6578  swoer  6809  elmapssres  6921  mapsspm  6930  pmsspw  6931  mapss  6940  dom0  7105  xpf1o  7111  sbthlemi8  7248  sbthlemi9  7249  fsuppimpd  7260  supelti  7307  supisoti  7315  djulclb  7360  nninfninc  7428  nnnninfeq2  7434  cardcl  7491  isnumi  7492  cardval3ex  7495  exmidonfinlem  7510  en2eleq  7512  finacn  7525  acfun  7528  exmidaclem  7529  pw1if  7549  papirr  7576  dftap2  7582  exmidapne  7591  ccfunen  7595  acnccim  7603  indpi  7674  dfplpq2  7686  ltbtwnnq  7748  enq0tr  7766  nqnq0pi  7770  elnp1st2nd  7808  prcunqu  7817  prnmaxl  7820  prloc  7823  genpcuu  7852  addnqprllem  7859  addlocprlemeq  7865  addlocprlemgt  7866  addlocpr  7868  nqprxx  7878  gtnqex  7882  appdivnq  7895  prmuloclemcalc  7897  prmuloc  7898  mullocprlem  7902  ltprordil  7921  ltnqpri  7926  ltexprlemm  7932  ltexprlemopl  7933  ltexprlemlol  7934  ltexprlemopu  7935  ltexprlemupu  7936  ltexprlemdisj  7938  ltexprlemloc  7939  ltexprlemfl  7941  ltexprlemrl  7942  ltexprlemfu  7943  ltexprlemru  7944  ltexpri  7945  recexprlemell  7954  recexprlemelu  7955  recexprlemloc  7963  recexprlempr  7964  recexprlem1ssl  7965  recexprlem1ssu  7966  recexprlemss1l  7967  aptipr  7973  cauappcvgprlemlol  7979  cauappcvgprlemupu  7981  cauappcvgprlemladdfu  7986  cauappcvgprlemladdfl  7987  cauappcvgprlemladdrl  7989  caucvgprlemnkj  7998  caucvgprlemnbj  7999  caucvgprlemlol  8002  caucvgprlemupu  8004  caucvgprlemladdfu  8009  caucvgprlem1  8011  caucvgprlem2  8012  caucvgprprlemnjltk  8023  caucvgprprlemnbj  8025  caucvgprprlemlol  8030  caucvgprprlemupu  8032  caucvgprprlemexbt  8038  caucvgprprlem1  8041  caucvgprprlem2  8042  suplocexprlemrl  8049  suplocexprlemru  8051  suplocexprlemdisj  8052  suplocexprlemub  8055  suplocexprlemlub  8056  ltsrprg  8079  gt0srpr  8080  recexgt0sr  8105  addgt0sr  8107  mulgt0sr  8110  map2psrprg  8137  suplocsrlemb  8138  suplocsrlem  8140  nnindnn  8225  axcaucvglemcau  8230  axpre-suploclemres  8233  apreap  8880  apreim  8896  mulge0  8912  apti  8915  mulap0bbd  8953  lble  9242  nnind  9274  recnz  9693  uzind  9711  eluzadd  9905  eluzsub  9906  ixxss1  10260  ixxss2  10261  ixxss12  10262  iccss2  10300  iccssioo2  10302  iccssico2  10303  elfzolt2  10517  infssuzcldc  10621  ioom  10648  elicore  10654  flqltp1  10667  addmodlteq  10788  expcl2lemap  10941  expap0i  10961  hashennnuni  11171  hashdmprop2dom  11245  wrdexb  11265  swrdsbslen  11387  swrdspsleq  11388  crre  11571  sq01  11609  caucvgre  11696  cvg1nlemcau  11699  cvg1nlemres  11700  resqrexlemoverl  11736  sqrtge0  11748  fimaxre2  11942  climi  12002  reccn2ap  12028  climge0  12040  nnf1o  12092  sumpr  12129  fsump1i  12149  fsum00  12178  fsumparts  12186  mertenslemi1  12251  addsin  12458  subsin  12459  addcos  12462  subcos  12463  sinbnd2  12470  cosbnd2  12471  sinltxirr  12477  dvdsaddre2b  12557  evenelz  12583  4dvdseven  12633  gcd0id  12705  gcd1  12713  bezoutlemstep  12723  dvdsgcdb  12739  mulgcd  12742  gcdzeq  12748  dvdsmulgcd  12751  sqgcd  12755  dvdssqlem  12756  bezoutr  12758  uzwodc  12763  nninfctlemfo  12766  lcmval  12790  lcmcllem  12794  lcmgcdlem  12804  lcmdvds  12806  lcmgcdeq  12810  lcmdvdsb  12811  mulgcddvds  12821  rpmulgcd2  12822  qredeu  12824  rpdvds  12826  divgcdcoprm0  12828  isprm3  12845  divgcdodd  12870  coprm  12871  rpexp  12880  sqrt2irr  12889  qdencl  12916  qeqnumdivden  12921  divnumden  12923  divdenle  12924  densq  12931  phimullem  12952  eulerthlem1  12954  eulerthlemrprm  12956  eulerthlemth  12959  prmdiveq  12963  prmdivdiv  12964  hashgcdeq  12967  phisum  12968  odzid  12972  reumodprminv  12981  oddn2prm  12989  pythagtriplem4  12996  pythagtriplem11  13002  pythagtriplem13  13004  pythagtriplem19  13010  pclemub  13015  pcprendvds2  13019  pcpre1  13020  pcpremul  13021  pceulem  13022  pczdvds  13042  pc2dvds  13058  pcaddlem  13067  pcmpt  13071  pcmpt2  13072  pcmptdvds  13073  pcprod  13074  pockthlem  13084  pockthg  13085  prmunb  13090  1arithlem4  13094  4sqlem7  13112  4sqlem8  13113  4sqlem9  13114  4sqlem10  13115  4sqlemffi  13124  4sqlem15  13133  4sqlem16  13134  4sqlem17  13135  4sqlem18  13136  ballotfilem2  13177  ballotfilemfc0  13181  ballotfilemfcc  13182  ballotfilemi1  13194  ballotfilemii  13195  ballotfilemic  13199  ballotfilem1c  13200  ballotfilemsf1o  13206  ballotfilemscr  13211  ballotfilemrv  13212  ballotfilemfrci  13220  ballotfilemfrceq  13221  ballotfilemrinv0  13225  ennnfonelemom  13248  ennnfonelemex  13254  ennnfonelemf1  13258  ctiunctlemu1st  13274  ctiunctlemu2nd  13275  fnpr2ob  13609  mgmlrid  13647  gsumfzval  13659  gsumval2  13665  mndrid  13702  grpinvcnv  13828  dfgrp3mlem  13858  eqglact  13983  ghmgrp2  14004  ghmlin  14006  ghmnsgpreima  14027  kerf1ghm  14032  gsumsplit0  14104  prdsmndd  14141  prdsgrpd  14144  prdsinvgd  14145  srgdilem  14217  srgdir  14223  srgridm  14228  ringdilem  14260  ringdir  14267  ringridm  14272  unitmulcl  14363  unitnegcl  14380  rhmmhm  14409  elrhmunit  14427  lringuplu  14446  subrgring  14475  subrg1cl  14480  qusrhm  14807  znunit  14938  znrrg  14939  psrbagfsupp  14950  psrbaglecl  14955  psrbagcon  14957  psrbagconcl  14958  psrelbas  14961  mplsubgfilemcl  14985  mplsubgfileminv  14986  inopn  14999  restbasg  15164  ssrest  15178  cntop2  15198  icnpimaex  15207  cnima  15216  lmfss  15240  lmtopcnp  15246  txhmeo  15315  txswaphmeo  15317  psmet0  15323  psmettri2  15324  blhalf  15404  bdxmet  15497  xmetxpbl  15504  ioo2bl  15547  tgioo  15550  cncfi  15574  rescncf  15577  cdivcncfap  15600  cnopnap  15607  divcncfap  15610  dedekindeulemeu  15618  dedekindicclemeu  15627  ivthinclemum  15631  ivthinclemlopn  15632  ivthinclemuopn  15634  ivthinclemdisj  15636  ivthdec  15640  ivthreinc  15641  limcimo  15661  cnplimcim  15663  cnplimclemr  15665  cnlimci  15669  limccnpcntop  15671  limccnp2lem  15672  limccnp2cntop  15673  limccoap  15674  reldvg  15675  dvbsssg  15682  dvfgg  15684  dvaddxxbr  15697  dvmulxxbr  15698  dvcoapbr  15703  dvcjbr  15704  dvrecap  15709  plyco  15755  plycj  15757  plyrecj  15759  sin0pilem1  15777  sin0pilem2  15778  tanrpcl  15833  tangtx  15834  cos0pilt1  15848  logbgcd1irraplemexp  15964  mpodvdsmulf1o  15989  perfect  16000  lgsne0  16042  lgseisen  16078  lgsquad2lem2  16086  2sqlem8a  16126  2sqlem8  16127  structgrssiedg  16169  uhgrm  16204  umgredgne  16276  usgruspgrben  16312  usgredgppren  16323  umgr2edg  16333  vtxdumgrfival  16424  wlkpropg  16450  wlkv  16452  wlkvtxeledgg  16470  g0wlk0  16496  trlsv  16510  clwwlknlen  16537  eupthv  16572  eupthf1o  16576  eupth2lem3lem4fi  16599  eulerpathprum  16606  bj-charfunbi  16722  bj-inf2vnlem1  16881  pwf1oexmid  16914  subctctexmid  16915  iooref1o  16959  taupi  16999  alsi2d  17008  alsc2d  17010