Theorem simpld 112

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
simpld	|- ( ph -> ps )

Proof of Theorem simpld

Step	Hyp	Ref	Expression
1		simpld.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  biimp  118  simplbi  274  simprbda  383  simprld  530  simp1  1021  eldifad  3209  unssad  3382  opth1  4326  opth  4327  0nelop  4338  epelg  4385  poirr  4402  brrelex1  4763  brrelex  4764  asymref  5120  soirri  5129  sotri  5130  ffdmd  5503  fcnvres  5517  fun11iun  5601  funopsn  5825  elmpocl1  6213  f1od  6221  f1o2d  6223  oprssdmm  6329  elmpom  6398  smoiso  6463  tfrlem1  6469  swoer  6725  ecopovtrn  6796  ecopovtrng  6799  elmapssres  6837  pmresg  6840  mapsspm  6846  en1uniel  6973  pw2f1odc  7016  xpf1o  7025  sbthlemi9  7155  supelti  7192  supsnti  7195  supisoti  7200  ctssdccl  7301  ctfoex  7308  fodjum  7336  en2eleq  7396  djuen  7416  pw1if  7433  dftap2  7460  2omotaplemst  7467  exmidapne  7469  ccfunen  7473  dfplpq2  7564  ltbtwnnqq  7625  enq0tr  7644  elnp1st2nd  7686  prcdnql  7694  prnminu  7699  prloc  7701  genpcdl  7729  addnqprulem  7738  addlocprlemlt  7741  addlocprlemgt  7744  addlocprlem  7745  addlocpr  7746  nqprxx  7756  ltnqex  7759  addnqprlemfl  7769  addnqprlemfu  7770  appdivnq  7773  prmuloclemcalc  7775  prmuloc  7776  mullocprlem  7780  mulnqprlemfl  7785  mulnqprlemfu  7786  ltprordil  7799  ltnqpri  7804  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  ltexpri  7823  lteupri  7827  ltaprlem  7828  recexprlemell  7832  recexprlemelu  7833  recexprlemloc  7841  recexprlempr  7842  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1u  7846  aptipr  7851  cauappcvgprlemm  7855  cauappcvgprlemlol  7857  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlem1  7869  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemlol  7880  caucvgprlemladdfu  7887  caucvgprprlemloccalc  7894  caucvgprprlemnkltj  7899  caucvgprprlemnbj  7903  caucvgprprlemml  7904  caucvgprprlemlol  7908  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  suplocexprlemss  7925  suplocexprlemru  7929  suplocexprlemlub  7934  ltsrprg  7957  caucvgsrlemasr  8000  suplocsrlemb  8016  suplocsrlem  8018  suplocsr  8019  axcaucvglemcau  8108  axpre-suploclemres  8111  negf1o  8551  apreap  8757  apreim  8773  msqge0  8786  mulge0  8789  apti  8792  apsscn  8817  mulap0bad  8829  divadddivap  8897  recnz  9563  lbzbi  9840  xadd4d  10110  ixxss1  10129  ixxss2  10130  ixxss12  10131  iccss2  10169  iccssioo2  10171  iccssico2  10172  iccen  10231  elfzole1  10381  ioom  10510  elicore  10516  flqle  10528  flqltnz  10537  addmodlteq  10650  expclzap  10816  hashennnuni  11031  zfz1isolem1  11094  hashdmprop2dom  11098  swrdsbslen  11237  ccatswrd  11241  ccatpfx  11272  recl  11404  cvg1nlemcau  11535  cvg1nlemres  11536  resqrtth  11582  fimaxre2  11778  climcl  11833  reccn2ap  11864  nnf1o  11927  summodclem3  11931  sumpr  11964  fsump1i  11984  fisumcom2  11989  fsum00  12013  fsumparts  12021  mertenslemi1  12086  prodmodclem3  12126  fprodcom2fi  12177  addsin  12293  subsin  12294  addcos  12297  subcos  12298  sinbnd2  12305  cosbnd2  12306  sin01gt0  12313  cos01gt0  12314  divgcdz  12532  divgcdnn  12536  gcdaddm  12545  bezoutlemstep  12558  dvdsgcdb  12574  dfgcd2  12575  mulgcd  12577  gcdzeq  12583  dvdsmulgcd  12586  sqgcd  12590  bezoutr  12593  lcmval  12625  lcmcllem  12629  gcddvdslcm  12635  lcmgcdlem  12639  lcmgcd  12640  lcmgcdeq  12645  lcmdvdsb  12646  mulgcddvds  12656  rpmulgcd2  12657  qredeu  12659  rpdvds  12661  isprm3  12680  divgcdodd  12705  coprm  12706  rpexp  12715  sqrt2irr  12724  qnumcl  12750  qnumdencoprm  12755  divnumden  12758  numsq  12765  phimullem  12787  eulerthlem1  12789  prmdiveq  12798  prmdivdiv  12799  hashgcdlem  12800  odzcl  12806  reumodprminv  12816  pythagtriplem19  12845  pclemub  12850  pcprendvds  12853  pcprendvds2  12854  pcpre1  12855  pcpremul  12856  pceulem  12857  pceu  12858  pczpre  12860  pczcl  12861  pcgcd1  12891  pc2dvds  12893  pcaddlem  12902  pcmpt  12906  pockthlem  12919  prmunb  12925  4sqlem7  12947  4sqlem8  12948  4sqlem9  12949  4sqlem10  12950  4sqlem14  12967  4sqlem15  12968  4sqlem16  12969  4sqlem17  12970  4sqlem18  12971  ennnfonelemg  13014  ennnfonelemf1  13029  ctiunctlemu1st  13045  nninfdclemf  13060  nninfdclemp1  13061  mgmidcl  13451  gsumfzval  13464  gsumval2  13470  mndlid  13508  prdsmndd  13521  imasmndf1  13527  dfgrp3mlem  13671  grplactf1o  13676  prdsgrpd  13682  prdsinvgd  13683  imasgrpf1  13689  subgsubm  13773  qusgrp  13809  ghmgrp1  13822  ghmf  13824  ghmnsgpreima  13846  kerf1ghm  13851  conjsubg  13854  imasrng  13959  srgdilem  13972  srgdi  13977  srglidm  13982  ringdilem  14015  ringdi  14021  ringlidm  14026  imasring  14067  imasringf1  14068  dvdsrcld  14101  unitcld  14112  unitmulcl  14117  unitnegcl  14134  rhmghm  14166  elrhmunit  14181  subrgss  14226  subrgrcl  14230  lmodvscl  14309  lmodvsdi  14315  lmodvsdir  14316  lsslsp  14433  qusring  14531  crngridl  14534  znunit  14663  znrrg  14664  psrbaglesuppg  14676  psrelbas  14679  psraddcl  14684  mplrcl  14698  uniopn  14715  restbasg  14882  cntop1  14915  cnf  14918  cnpf2  14921  lmtopcnp  14964  psmetdmdm  15038  psmetf  15039  psmet0  15041  xmetf  15064  metf  15065  blhalf  15122  xmetxpbl  15222  ioo2bl  15265  tgioo  15268  cncff  15291  rescncf  15295  cdivcncfap  15318  cnopnap  15325  divcncfap  15328  dedekindeulemeu  15336  dedekindicclemeu  15345  ivthinclemlm  15348  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthinclemdisj  15354  ivthdec  15358  ivthreinc  15359  limcimolemlt  15378  limcimo  15379  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  limccoap  15392  eldvap  15396  dvbsssg  15400  dvfgg  15402  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcj  15423  dvfre  15424  dvrecap  15427  plyco  15473  plycj  15475  sin0pilem1  15495  sin0pilem2  15496  pilem3  15497  tanrpcl  15551  tangtx  15552  perfect  15715  lgsne0  15757  lgseisen  15793  lgsquad2lem2  15801  2sqlem8a  15841  2sqlem8  15842  structgrssvtx  15883  edguhgr  15976  umgrpredgv  15986  umgrnloop2  15990  umgr2edg  16046  wlkpropg  16121  wlkv  16123  wlkvtxeledgg  16141  wlkvtxiedgg  16143  wlk1walkdom  16156  trlsv  16179  clwwlksswrd  16192  clwwlkclwwlkn  16204  eupthv  16241  eupthseg  16247  nninfalllem1  16546  iooref1o  16574  alsi1d  16621  alsc1d  16623