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:  biimp  117  simplbi  272  simprbda  381  simp1  982  eldifad  3113  unssad  3284  opth1  4196  opth  4197  0nelop  4208  epelg  4250  poirr  4267  brrelex1  4625  brrelex  4626  asymref  4971  soirri  4980  sotri  4981  fcnvres  5353  fun11iun  5435  elmpocl1  6019  f1od  6023  f1o2d  6025  oprssdmm  6119  smoiso  6249  tfrlem1  6255  swoer  6508  ecopovtrn  6577  ecopovtrng  6580  elmapssres  6618  pmresg  6621  mapsspm  6627  en1uniel  6749  xpf1o  6789  sbthlemi9  6909  supelti  6946  supsnti  6949  supisoti  6954  ctssdccl  7055  ctfoex  7062  fodjum  7089  en2eleq  7130  djuen  7146  ccfunen  7184  dfplpq2  7274  ltbtwnnqq  7335  enq0tr  7354  elnp1st2nd  7396  prcdnql  7404  prnminu  7409  prloc  7411  genpcdl  7439  addnqprulem  7448  addlocprlemlt  7451  addlocprlemgt  7454  addlocprlem  7455  addlocpr  7456  nqprxx  7466  ltnqex  7469  addnqprlemfl  7479  addnqprlemfu  7480  appdivnq  7483  prmuloclemcalc  7485  prmuloc  7486  mullocprlem  7490  mulnqprlemfl  7495  mulnqprlemfu  7496  ltprordil  7509  ltnqpri  7514  ltexprlemm  7520  ltexprlemopl  7521  ltexprlemlol  7522  ltexprlemopu  7523  ltexprlemupu  7524  ltexprlemdisj  7526  ltexprlemloc  7527  ltexprlemfl  7529  ltexprlemrl  7530  ltexprlemfu  7531  ltexprlemru  7532  ltexpri  7533  lteupri  7537  ltaprlem  7538  recexprlemell  7542  recexprlemelu  7543  recexprlemloc  7551  recexprlempr  7552  recexprlem1ssl  7553  recexprlem1ssu  7554  recexprlemss1u  7556  aptipr  7561  cauappcvgprlemm  7565  cauappcvgprlemlol  7567  cauappcvgprlemladdfu  7574  cauappcvgprlemladdfl  7575  cauappcvgprlemladdru  7576  cauappcvgprlem1  7579  caucvgprlemnkj  7586  caucvgprlemnbj  7587  caucvgprlemm  7588  caucvgprlemlol  7590  caucvgprlemladdfu  7597  caucvgprprlemloccalc  7604  caucvgprprlemnkltj  7609  caucvgprprlemnbj  7613  caucvgprprlemml  7614  caucvgprprlemlol  7618  caucvgprprlemloc  7623  caucvgprprlemexbt  7626  suplocexprlemss  7635  suplocexprlemru  7639  suplocexprlemlub  7644  ltsrprg  7667  caucvgsrlemasr  7710  suplocsrlemb  7726  suplocsrlem  7728  suplocsr  7729  axcaucvglemcau  7818  axpre-suploclemres  7821  negf1o  8257  apreap  8462  apreim  8478  msqge0  8491  mulge0  8494  apti  8497  apsscn  8522  mulap0bad  8533  divadddivap  8600  recnz  9257  lbzbi  9525  xadd4d  9789  ixxss1  9808  ixxss2  9809  ixxss12  9810  iccss2  9848  iccssioo2  9850  iccssico2  9851  iccen  9910  elfzole1  10054  ioom  10160  elicore  10166  flqle  10177  flqltnz  10186  addmodlteq  10297  expclzap  10444  hashennnuni  10653  zfz1isolem1  10711  recl  10753  cvg1nlemcau  10884  cvg1nlemres  10885  resqrtth  10931  fimaxre2  11126  climcl  11179  reccn2ap  11210  nnf1o  11273  summodclem3  11277  sumpr  11310  fsump1i  11330  fisumcom2  11335  fsum00  11359  fsumparts  11367  mertenslemi1  11432  prodmodclem3  11472  fprodcom2fi  11523  addsin  11639  subsin  11640  addcos  11643  subcos  11644  sinbnd2  11651  cosbnd2  11652  sin01gt0  11658  cos01gt0  11659  divgcdz  11855  divgcdnn  11859  gcdaddm  11868  bezoutlemstep  11881  dvdsgcdb  11897  dfgcd2  11898  mulgcd  11900  gcdzeq  11906  dvdsmulgcd  11909  sqgcd  11913  bezoutr  11916  lcmval  11940  lcmcllem  11944  gcddvdslcm  11950  lcmgcdlem  11954  lcmgcd  11955  lcmgcdeq  11960  lcmdvdsb  11961  mulgcddvds  11971  rpmulgcd2  11972  qredeu  11974  rpdvds  11976  isprm3  11995  divgcdodd  12018  coprm  12019  rpexp  12028  sqrt2irr  12037  qnumcl  12063  qnumdencoprm  12068  divnumden  12071  numsq  12078  phimullem  12100  eulerthlem1  12102  prmdiveq  12111  prmdivdiv  12112  hashgcdlem  12113  odzcl  12118  reumodprminv  12128  ennnfonelemg  12143  ennnfonelemf1  12158  ctiunctlemu1st  12174  nninfdclemf  12191  nninfdclemp1  12192  uniopn  12410  restbasg  12579  cntop1  12612  cnf  12615  cnpf2  12618  lmtopcnp  12661  psmetdmdm  12735  psmetf  12736  psmet0  12738  xmetf  12761  metf  12762  blhalf  12819  xmetxpbl  12919  ioo2bl  12954  tgioo  12957  cncff  12975  rescncf  12979  cdivcncfap  12998  cnopnap  13005  dedekindeulemeu  13011  dedekindicclemeu  13020  ivthinclemlm  13023  ivthinclemlopn  13025  ivthinclemuopn  13027  ivthinclemdisj  13029  ivthdec  13033  limcimolemlt  13044  limcimo  13045  limccnpcntop  13055  limccnp2lem  13056  limccnp2cntop  13057  limccoap  13058  eldvap  13062  dvbsssg  13066  dvfgg  13068  dvaddxxbr  13076  dvmulxxbr  13077  dvcoapbr  13082  dvcj  13084  dvfre  13085  dvrecap  13088  sin0pilem1  13113  sin0pilem2  13114  pilem3  13115  tanrpcl  13169  tangtx  13170  nninfalllem1  13591  iooref1o  13616  alsi1d  13660  alsc1d  13662