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  997  eldifad  3140  unssad  3312  opth1  4234  opth  4235  0nelop  4246  epelg  4288  poirr  4305  brrelex1  4663  brrelex  4664  asymref  5011  soirri  5020  sotri  5021  fcnvres  5396  fun11iun  5479  elmpocl1  6065  f1od  6069  f1o2d  6071  oprssdmm  6167  smoiso  6298  tfrlem1  6304  swoer  6558  ecopovtrn  6627  ecopovtrng  6630  elmapssres  6668  pmresg  6671  mapsspm  6677  en1uniel  6799  xpf1o  6839  sbthlemi9  6959  supelti  6996  supsnti  6999  supisoti  7004  ctssdccl  7105  ctfoex  7112  fodjum  7139  en2eleq  7189  djuen  7205  dftap2  7245  2omotaplemst  7252  exmidapne  7254  ccfunen  7258  dfplpq2  7348  ltbtwnnqq  7409  enq0tr  7428  elnp1st2nd  7470  prcdnql  7478  prnminu  7483  prloc  7485  genpcdl  7513  addnqprulem  7522  addlocprlemlt  7525  addlocprlemgt  7528  addlocprlem  7529  addlocpr  7530  nqprxx  7540  ltnqex  7543  addnqprlemfl  7553  addnqprlemfu  7554  appdivnq  7557  prmuloclemcalc  7559  prmuloc  7560  mullocprlem  7564  mulnqprlemfl  7569  mulnqprlemfu  7570  ltprordil  7583  ltnqpri  7588  ltexprlemm  7594  ltexprlemopl  7595  ltexprlemlol  7596  ltexprlemopu  7597  ltexprlemupu  7598  ltexprlemdisj  7600  ltexprlemloc  7601  ltexprlemfl  7603  ltexprlemrl  7604  ltexprlemfu  7605  ltexprlemru  7606  ltexpri  7607  lteupri  7611  ltaprlem  7612  recexprlemell  7616  recexprlemelu  7617  recexprlemloc  7625  recexprlempr  7626  recexprlem1ssl  7627  recexprlem1ssu  7628  recexprlemss1u  7630  aptipr  7635  cauappcvgprlemm  7639  cauappcvgprlemlol  7641  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlemladdru  7650  cauappcvgprlem1  7653  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemm  7662  caucvgprlemlol  7664  caucvgprlemladdfu  7671  caucvgprprlemloccalc  7678  caucvgprprlemnkltj  7683  caucvgprprlemnbj  7687  caucvgprprlemml  7688  caucvgprprlemlol  7692  caucvgprprlemloc  7697  caucvgprprlemexbt  7700  suplocexprlemss  7709  suplocexprlemru  7713  suplocexprlemlub  7718  ltsrprg  7741  caucvgsrlemasr  7784  suplocsrlemb  7800  suplocsrlem  7802  suplocsr  7803  axcaucvglemcau  7892  axpre-suploclemres  7895  negf1o  8333  apreap  8538  apreim  8554  msqge0  8567  mulge0  8570  apti  8573  apsscn  8598  mulap0bad  8610  divadddivap  8678  recnz  9340  lbzbi  9610  xadd4d  9879  ixxss1  9898  ixxss2  9899  ixxss12  9900  iccss2  9938  iccssioo2  9940  iccssico2  9941  iccen  10000  elfzole1  10148  ioom  10254  elicore  10260  flqle  10271  flqltnz  10280  addmodlteq  10391  expclzap  10538  hashennnuni  10750  zfz1isolem1  10811  recl  10853  cvg1nlemcau  10984  cvg1nlemres  10985  resqrtth  11031  fimaxre2  11226  climcl  11281  reccn2ap  11312  nnf1o  11375  summodclem3  11379  sumpr  11412  fsump1i  11432  fisumcom2  11437  fsum00  11461  fsumparts  11469  mertenslemi1  11534  prodmodclem3  11574  fprodcom2fi  11625  addsin  11741  subsin  11742  addcos  11745  subcos  11746  sinbnd2  11753  cosbnd2  11754  sin01gt0  11760  cos01gt0  11761  divgcdz  11962  divgcdnn  11966  gcdaddm  11975  bezoutlemstep  11988  dvdsgcdb  12004  dfgcd2  12005  mulgcd  12007  gcdzeq  12013  dvdsmulgcd  12016  sqgcd  12020  bezoutr  12023  lcmval  12053  lcmcllem  12057  gcddvdslcm  12063  lcmgcdlem  12067  lcmgcd  12068  lcmgcdeq  12073  lcmdvdsb  12074  mulgcddvds  12084  rpmulgcd2  12085  qredeu  12087  rpdvds  12089  isprm3  12108  divgcdodd  12133  coprm  12134  rpexp  12143  sqrt2irr  12152  qnumcl  12178  qnumdencoprm  12183  divnumden  12186  numsq  12193  phimullem  12215  eulerthlem1  12217  prmdiveq  12226  prmdivdiv  12227  hashgcdlem  12228  odzcl  12233  reumodprminv  12243  pythagtriplem19  12272  pclemub  12277  pcprendvds  12280  pcprendvds2  12281  pcpre1  12282  pcpremul  12283  pceulem  12284  pceu  12285  pczpre  12287  pczcl  12288  pcgcd1  12317  pc2dvds  12319  pcaddlem  12328  pcmpt  12331  pockthlem  12344  prmunb  12350  4sqlem7  12372  4sqlem8  12373  4sqlem9  12374  4sqlem10  12375  ennnfonelemg  12394  ennnfonelemf1  12409  ctiunctlemu1st  12425  nninfdclemf  12440  nninfdclemp1  12441  mgmidcl  12727  mndlid  12766  dfgrp3mlem  12896  grplactf1o  12901  subgsubm  12982  srgdilem  13052  srgdi  13057  srglidm  13062  ringdilem  13095  ringdi  13101  ringlidm  13106  dvdsrcld  13165  unitcld  13176  unitmulcl  13181  unitnegcl  13198  uniopn  13281  restbasg  13450  cntop1  13483  cnf  13486  cnpf2  13489  lmtopcnp  13532  psmetdmdm  13606  psmetf  13607  psmet0  13609  xmetf  13632  metf  13633  blhalf  13690  xmetxpbl  13790  ioo2bl  13825  tgioo  13828  cncff  13846  rescncf  13850  cdivcncfap  13869  cnopnap  13876  dedekindeulemeu  13882  dedekindicclemeu  13891  ivthinclemlm  13894  ivthinclemlopn  13896  ivthinclemuopn  13898  ivthinclemdisj  13900  ivthdec  13904  limcimolemlt  13915  limcimo  13916  limccnpcntop  13926  limccnp2lem  13927  limccnp2cntop  13928  limccoap  13929  eldvap  13933  dvbsssg  13937  dvfgg  13939  dvaddxxbr  13947  dvmulxxbr  13948  dvcoapbr  13953  dvcj  13955  dvfre  13956  dvrecap  13959  sin0pilem1  13984  sin0pilem2  13985  pilem3  13986  tanrpcl  14040  tangtx  14041  lgsne0  14221  2sqlem8a  14240  2sqlem8  14241  nninfalllem1  14528  iooref1o  14553  alsi1d  14599  alsc1d  14601