Theorem simpld 111

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  bi1  117  simplbi  272  simprbda  380  simp1  981  eldifad  3082  unssad  3253  opth1  4158  opth  4159  0nelop  4170  epelg  4212  poirr  4229  brrelex1  4578  brrelex  4579  asymref  4924  soirri  4933  sotri  4934  fcnvres  5306  fun11iun  5388  elmpocl1  5969  f1od  5973  f1o2d  5975  oprssdmm  6069  smoiso  6199  tfrlem1  6205  swoer  6457  ecopovtrn  6526  ecopovtrng  6529  elmapssres  6567  pmresg  6570  mapsspm  6576  en1uniel  6698  xpf1o  6738  sbthlemi9  6853  supelti  6889  supsnti  6892  supisoti  6897  ctssdccl  6996  ctfoex  7003  fodjum  7018  en2eleq  7051  djuen  7067  ccfunen  7079  dfplpq2  7162  ltbtwnnqq  7223  enq0tr  7242  elnp1st2nd  7284  prcdnql  7292  prnminu  7297  prloc  7299  genpcdl  7327  addnqprulem  7336  addlocprlemlt  7339  addlocprlemgt  7342  addlocprlem  7343  addlocpr  7344  nqprxx  7354  ltnqex  7357  addnqprlemfl  7367  addnqprlemfu  7368  appdivnq  7371  prmuloclemcalc  7373  prmuloc  7374  mullocprlem  7378  mulnqprlemfl  7383  mulnqprlemfu  7384  ltprordil  7397  ltnqpri  7402  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  ltexpri  7421  lteupri  7425  ltaprlem  7426  recexprlemell  7430  recexprlemelu  7431  recexprlemloc  7439  recexprlempr  7440  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1u  7444  aptipr  7449  cauappcvgprlemm  7453  cauappcvgprlemlol  7455  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlem1  7467  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemlol  7478  caucvgprlemladdfu  7485  caucvgprprlemloccalc  7492  caucvgprprlemnkltj  7497  caucvgprprlemnbj  7501  caucvgprprlemml  7502  caucvgprprlemlol  7506  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  suplocexprlemss  7523  suplocexprlemru  7527  suplocexprlemlub  7532  ltsrprg  7555  caucvgsrlemasr  7598  suplocsrlemb  7614  suplocsrlem  7616  suplocsr  7617  axcaucvglemcau  7706  axpre-suploclemres  7709  negf1o  8144  apreap  8349  apreim  8365  msqge0  8378  mulge0  8381  apti  8384  apsscn  8409  mulap0bad  8420  divadddivap  8487  recnz  9144  lbzbi  9408  xadd4d  9668  ixxss1  9687  ixxss2  9688  ixxss12  9689  iccss2  9727  iccssioo2  9729  iccssico2  9730  elfzole1  9932  ioom  10038  flqle  10051  flqltnz  10060  addmodlteq  10171  expclzap  10318  hashennnuni  10525  zfz1isolem1  10583  recl  10625  cvg1nlemcau  10756  cvg1nlemres  10757  resqrtth  10803  fimaxre2  10998  climcl  11051  reccn2ap  11082  nnf1o  11145  summodclem3  11149  sumpr  11182  fsump1i  11202  fisumcom2  11207  fsum00  11231  fsumparts  11239  mertenslemi1  11304  prodmodclem3  11344  addsin  11449  subsin  11450  addcos  11453  subcos  11454  sinbnd2  11461  cosbnd2  11462  sin01gt0  11468  cos01gt0  11469  divgcdz  11660  divgcdnn  11663  gcdaddm  11672  bezoutlemstep  11685  dvdsgcdb  11701  dfgcd2  11702  mulgcd  11704  gcdzeq  11710  dvdsmulgcd  11713  sqgcd  11717  bezoutr  11720  lcmval  11744  lcmcllem  11748  gcddvdslcm  11754  lcmgcdlem  11758  lcmgcd  11759  lcmgcdeq  11764  lcmdvdsb  11765  mulgcddvds  11775  rpmulgcd2  11776  qredeu  11778  rpdvds  11780  isprm3  11799  divgcdodd  11821  coprm  11822  rpexp  11831  sqrt2irr  11840  qnumcl  11866  qnumdencoprm  11871  divnumden  11874  numsq  11881  phimullem  11901  hashgcdlem  11903  ennnfonelemg  11916  ennnfonelemf1  11931  ctiunctlemu1st  11947  uniopn  12168  restbasg  12337  cntop1  12370  cnf  12373  cnpf2  12376  lmtopcnp  12419  psmetdmdm  12493  psmetf  12494  psmet0  12496  xmetf  12519  metf  12520  blhalf  12577  xmetxpbl  12677  ioo2bl  12712  tgioo  12715  cncff  12733  rescncf  12737  cdivcncfap  12756  cnopnap  12763  dedekindeulemeu  12769  dedekindicclemeu  12778  ivthinclemlm  12781  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthinclemdisj  12787  ivthdec  12791  limcimolemlt  12802  limcimo  12803  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  limccoap  12816  eldvap  12820  dvbsssg  12824  dvfgg  12826  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcj  12842  dvfre  12843  dvrecap  12846  sin0pilem1  12862  sin0pilem2  12863  pilem3  12864  tanrpcl  12918  tangtx  12919  nninfalllem1  13203  alsi1d  13247  alsc1d  13249