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  999  eldifad  3164  unssad  3336  opth1  4265  opth  4266  0nelop  4277  epelg  4321  poirr  4338  brrelex1  4698  brrelex  4699  asymref  5051  soirri  5060  sotri  5061  fcnvres  5437  fun11iun  5521  elmpocl1  6114  f1od  6121  f1o2d  6123  oprssdmm  6224  smoiso  6355  tfrlem1  6361  swoer  6615  ecopovtrn  6686  ecopovtrng  6689  elmapssres  6727  pmresg  6730  mapsspm  6736  en1uniel  6858  pw2f1odc  6891  xpf1o  6900  sbthlemi9  7024  supelti  7061  supsnti  7064  supisoti  7069  ctssdccl  7170  ctfoex  7177  fodjum  7205  en2eleq  7255  djuen  7271  dftap2  7311  2omotaplemst  7318  exmidapne  7320  ccfunen  7324  dfplpq2  7414  ltbtwnnqq  7475  enq0tr  7494  elnp1st2nd  7536  prcdnql  7544  prnminu  7549  prloc  7551  genpcdl  7579  addnqprulem  7588  addlocprlemlt  7591  addlocprlemgt  7594  addlocprlem  7595  addlocpr  7596  nqprxx  7606  ltnqex  7609  addnqprlemfl  7619  addnqprlemfu  7620  appdivnq  7623  prmuloclemcalc  7625  prmuloc  7626  mullocprlem  7630  mulnqprlemfl  7635  mulnqprlemfu  7636  ltprordil  7649  ltnqpri  7654  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemfl  7669  ltexprlemrl  7670  ltexprlemfu  7671  ltexprlemru  7672  ltexpri  7673  lteupri  7677  ltaprlem  7678  recexprlemell  7682  recexprlemelu  7683  recexprlemloc  7691  recexprlempr  7692  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1u  7696  aptipr  7701  cauappcvgprlemm  7705  cauappcvgprlemlol  7707  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlem1  7719  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemlol  7730  caucvgprlemladdfu  7737  caucvgprprlemloccalc  7744  caucvgprprlemnkltj  7749  caucvgprprlemnbj  7753  caucvgprprlemml  7754  caucvgprprlemlol  7758  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  suplocexprlemss  7775  suplocexprlemru  7779  suplocexprlemlub  7784  ltsrprg  7807  caucvgsrlemasr  7850  suplocsrlemb  7866  suplocsrlem  7868  suplocsr  7869  axcaucvglemcau  7958  axpre-suploclemres  7961  negf1o  8401  apreap  8606  apreim  8622  msqge0  8635  mulge0  8638  apti  8641  apsscn  8666  mulap0bad  8678  divadddivap  8746  recnz  9410  lbzbi  9681  xadd4d  9951  ixxss1  9970  ixxss2  9971  ixxss12  9972  iccss2  10010  iccssioo2  10012  iccssico2  10013  iccen  10072  elfzole1  10222  ioom  10329  elicore  10335  flqle  10347  flqltnz  10356  addmodlteq  10469  expclzap  10635  hashennnuni  10850  zfz1isolem1  10911  recl  10997  cvg1nlemcau  11128  cvg1nlemres  11129  resqrtth  11175  fimaxre2  11370  climcl  11425  reccn2ap  11456  nnf1o  11519  summodclem3  11523  sumpr  11556  fsump1i  11576  fisumcom2  11581  fsum00  11605  fsumparts  11613  mertenslemi1  11678  prodmodclem3  11718  fprodcom2fi  11769  addsin  11885  subsin  11886  addcos  11889  subcos  11890  sinbnd2  11897  cosbnd2  11898  sin01gt0  11905  cos01gt0  11906  divgcdz  12108  divgcdnn  12112  gcdaddm  12121  bezoutlemstep  12134  dvdsgcdb  12150  dfgcd2  12151  mulgcd  12153  gcdzeq  12159  dvdsmulgcd  12162  sqgcd  12166  bezoutr  12169  lcmval  12201  lcmcllem  12205  gcddvdslcm  12211  lcmgcdlem  12215  lcmgcd  12216  lcmgcdeq  12221  lcmdvdsb  12222  mulgcddvds  12232  rpmulgcd2  12233  qredeu  12235  rpdvds  12237  isprm3  12256  divgcdodd  12281  coprm  12282  rpexp  12291  sqrt2irr  12300  qnumcl  12326  qnumdencoprm  12331  divnumden  12334  numsq  12341  phimullem  12363  eulerthlem1  12365  prmdiveq  12374  prmdivdiv  12375  hashgcdlem  12376  odzcl  12381  reumodprminv  12391  pythagtriplem19  12420  pclemub  12425  pcprendvds  12428  pcprendvds2  12429  pcpre1  12430  pcpremul  12431  pceulem  12432  pceu  12433  pczpre  12435  pczcl  12436  pcgcd1  12466  pc2dvds  12468  pcaddlem  12477  pcmpt  12481  pockthlem  12494  prmunb  12500  4sqlem7  12522  4sqlem8  12523  4sqlem9  12524  4sqlem10  12525  4sqlem14  12542  4sqlem15  12543  4sqlem16  12544  4sqlem17  12545  4sqlem18  12546  ennnfonelemg  12560  ennnfonelemf1  12575  ctiunctlemu1st  12591  nninfdclemf  12606  nninfdclemp1  12607  mgmidcl  12961  gsumfzval  12974  gsumval2  12980  mndlid  13016  dfgrp3mlem  13170  grplactf1o  13175  imasgrpf1  13182  subgsubm  13266  qusgrp  13302  ghmgrp1  13315  ghmf  13317  ghmnsgpreima  13339  kerf1ghm  13344  conjsubg  13347  imasrng  13452  srgdilem  13465  srgdi  13470  srglidm  13475  ringdilem  13508  ringdi  13514  ringlidm  13519  imasring  13560  imasringf1  13561  dvdsrcld  13593  unitcld  13604  unitmulcl  13609  unitnegcl  13626  rhmghm  13658  elrhmunit  13673  subrgss  13718  subrgrcl  13722  lmodvscl  13801  lmodvsdi  13807  lmodvsdir  13808  lsslsp  13925  qusring  14023  crngridl  14026  znunit  14147  znrrg  14148  psrbaglesuppg  14158  psrelbas  14160  psraddcl  14164  uniopn  14169  restbasg  14336  cntop1  14369  cnf  14372  cnpf2  14375  lmtopcnp  14418  psmetdmdm  14492  psmetf  14493  psmet0  14495  xmetf  14518  metf  14519  blhalf  14576  xmetxpbl  14676  ioo2bl  14711  tgioo  14714  cncff  14732  rescncf  14736  cdivcncfap  14758  cnopnap  14765  divcncfap  14768  dedekindeulemeu  14776  dedekindicclemeu  14785  ivthinclemlm  14788  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthinclemdisj  14794  ivthdec  14798  ivthreinc  14799  limcimolemlt  14818  limcimo  14819  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  limccoap  14832  eldvap  14836  dvbsssg  14840  dvfgg  14842  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcj  14858  dvfre  14859  dvrecap  14862  sin0pilem1  14916  sin0pilem2  14917  pilem3  14918  tanrpcl  14972  tangtx  14973  lgsne0  15154  lgseisen  15190  2sqlem8a  15209  2sqlem8  15210  nninfalllem1  15498  iooref1o  15524  alsi1d  15571  alsc1d  15573