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  3142  unssad  3314  opth1  4238  opth  4239  0nelop  4250  epelg  4292  poirr  4309  brrelex1  4667  brrelex  4668  asymref  5016  soirri  5025  sotri  5026  fcnvres  5401  fun11iun  5484  elmpocl1  6073  f1od  6077  f1o2d  6079  oprssdmm  6175  smoiso  6306  tfrlem1  6312  swoer  6566  ecopovtrn  6635  ecopovtrng  6638  elmapssres  6676  pmresg  6679  mapsspm  6685  en1uniel  6807  xpf1o  6847  sbthlemi9  6967  supelti  7004  supsnti  7007  supisoti  7012  ctssdccl  7113  ctfoex  7120  fodjum  7147  en2eleq  7197  djuen  7213  dftap2  7253  2omotaplemst  7260  exmidapne  7262  ccfunen  7266  dfplpq2  7356  ltbtwnnqq  7417  enq0tr  7436  elnp1st2nd  7478  prcdnql  7486  prnminu  7491  prloc  7493  genpcdl  7521  addnqprulem  7530  addlocprlemlt  7533  addlocprlemgt  7536  addlocprlem  7537  addlocpr  7538  nqprxx  7548  ltnqex  7551  addnqprlemfl  7561  addnqprlemfu  7562  appdivnq  7565  prmuloclemcalc  7567  prmuloc  7568  mullocprlem  7572  mulnqprlemfl  7577  mulnqprlemfu  7578  ltprordil  7591  ltnqpri  7596  ltexprlemm  7602  ltexprlemopl  7603  ltexprlemlol  7604  ltexprlemopu  7605  ltexprlemupu  7606  ltexprlemdisj  7608  ltexprlemloc  7609  ltexprlemfl  7611  ltexprlemrl  7612  ltexprlemfu  7613  ltexprlemru  7614  ltexpri  7615  lteupri  7619  ltaprlem  7620  recexprlemell  7624  recexprlemelu  7625  recexprlemloc  7633  recexprlempr  7634  recexprlem1ssl  7635  recexprlem1ssu  7636  recexprlemss1u  7638  aptipr  7643  cauappcvgprlemm  7647  cauappcvgprlemlol  7649  cauappcvgprlemladdfu  7656  cauappcvgprlemladdfl  7657  cauappcvgprlemladdru  7658  cauappcvgprlem1  7661  caucvgprlemnkj  7668  caucvgprlemnbj  7669  caucvgprlemm  7670  caucvgprlemlol  7672  caucvgprlemladdfu  7679  caucvgprprlemloccalc  7686  caucvgprprlemnkltj  7691  caucvgprprlemnbj  7695  caucvgprprlemml  7696  caucvgprprlemlol  7700  caucvgprprlemloc  7705  caucvgprprlemexbt  7708  suplocexprlemss  7717  suplocexprlemru  7721  suplocexprlemlub  7726  ltsrprg  7749  caucvgsrlemasr  7792  suplocsrlemb  7808  suplocsrlem  7810  suplocsr  7811  axcaucvglemcau  7900  axpre-suploclemres  7903  negf1o  8342  apreap  8547  apreim  8563  msqge0  8576  mulge0  8579  apti  8582  apsscn  8607  mulap0bad  8619  divadddivap  8687  recnz  9349  lbzbi  9619  xadd4d  9888  ixxss1  9907  ixxss2  9908  ixxss12  9909  iccss2  9947  iccssioo2  9949  iccssico2  9950  iccen  10009  elfzole1  10158  ioom  10264  elicore  10270  flqle  10281  flqltnz  10290  addmodlteq  10401  expclzap  10548  hashennnuni  10762  zfz1isolem1  10823  recl  10865  cvg1nlemcau  10996  cvg1nlemres  10997  resqrtth  11043  fimaxre2  11238  climcl  11293  reccn2ap  11324  nnf1o  11387  summodclem3  11391  sumpr  11424  fsump1i  11444  fisumcom2  11449  fsum00  11473  fsumparts  11481  mertenslemi1  11546  prodmodclem3  11586  fprodcom2fi  11637  addsin  11753  subsin  11754  addcos  11757  subcos  11758  sinbnd2  11765  cosbnd2  11766  sin01gt0  11772  cos01gt0  11773  divgcdz  11975  divgcdnn  11979  gcdaddm  11988  bezoutlemstep  12001  dvdsgcdb  12017  dfgcd2  12018  mulgcd  12020  gcdzeq  12026  dvdsmulgcd  12029  sqgcd  12033  bezoutr  12036  lcmval  12066  lcmcllem  12070  gcddvdslcm  12076  lcmgcdlem  12080  lcmgcd  12081  lcmgcdeq  12086  lcmdvdsb  12087  mulgcddvds  12097  rpmulgcd2  12098  qredeu  12100  rpdvds  12102  isprm3  12121  divgcdodd  12146  coprm  12147  rpexp  12156  sqrt2irr  12165  qnumcl  12191  qnumdencoprm  12196  divnumden  12199  numsq  12206  phimullem  12228  eulerthlem1  12230  prmdiveq  12239  prmdivdiv  12240  hashgcdlem  12241  odzcl  12246  reumodprminv  12256  pythagtriplem19  12285  pclemub  12290  pcprendvds  12293  pcprendvds2  12294  pcpre1  12295  pcpremul  12296  pceulem  12297  pceu  12298  pczpre  12300  pczcl  12301  pcgcd1  12330  pc2dvds  12332  pcaddlem  12341  pcmpt  12344  pockthlem  12357  prmunb  12363  4sqlem7  12385  4sqlem8  12386  4sqlem9  12387  4sqlem10  12388  ennnfonelemg  12407  ennnfonelemf1  12422  ctiunctlemu1st  12438  nninfdclemf  12453  nninfdclemp1  12454  mgmidcl  12804  mndlid  12843  dfgrp3mlem  12975  grplactf1o  12980  subgsubm  13066  srgdilem  13163  srgdi  13168  srglidm  13173  ringdilem  13206  ringdi  13212  ringlidm  13217  dvdsrcld  13277  unitcld  13288  unitmulcl  13293  unitnegcl  13310  subrgss  13354  subrgrcl  13358  lmodvscl  13406  lmodvsdi  13412  lmodvsdir  13413  lsslsp  13527  uniopn  13662  restbasg  13829  cntop1  13862  cnf  13865  cnpf2  13868  lmtopcnp  13911  psmetdmdm  13985  psmetf  13986  psmet0  13988  xmetf  14011  metf  14012  blhalf  14069  xmetxpbl  14169  ioo2bl  14204  tgioo  14207  cncff  14225  rescncf  14229  cdivcncfap  14248  cnopnap  14255  dedekindeulemeu  14261  dedekindicclemeu  14270  ivthinclemlm  14273  ivthinclemlopn  14275  ivthinclemuopn  14277  ivthinclemdisj  14279  ivthdec  14283  limcimolemlt  14294  limcimo  14295  limccnpcntop  14305  limccnp2lem  14306  limccnp2cntop  14307  limccoap  14308  eldvap  14312  dvbsssg  14316  dvfgg  14318  dvaddxxbr  14326  dvmulxxbr  14327  dvcoapbr  14332  dvcj  14334  dvfre  14335  dvrecap  14338  sin0pilem1  14363  sin0pilem2  14364  pilem3  14365  tanrpcl  14419  tangtx  14420  lgsne0  14600  2sqlem8a  14630  2sqlem8  14631  nninfalllem1  14919  iooref1o  14944  alsi1d  14991  alsc1d  14993