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  992  eldifad  3132  unssad  3304  opth1  4221  opth  4222  0nelop  4233  epelg  4275  poirr  4292  brrelex1  4650  brrelex  4651  asymref  4996  soirri  5005  sotri  5006  fcnvres  5381  fun11iun  5463  elmpocl1  6048  f1od  6052  f1o2d  6054  oprssdmm  6150  smoiso  6281  tfrlem1  6287  swoer  6541  ecopovtrn  6610  ecopovtrng  6613  elmapssres  6651  pmresg  6654  mapsspm  6660  en1uniel  6782  xpf1o  6822  sbthlemi9  6942  supelti  6979  supsnti  6982  supisoti  6987  ctssdccl  7088  ctfoex  7095  fodjum  7122  en2eleq  7172  djuen  7188  ccfunen  7226  dfplpq2  7316  ltbtwnnqq  7377  enq0tr  7396  elnp1st2nd  7438  prcdnql  7446  prnminu  7451  prloc  7453  genpcdl  7481  addnqprulem  7490  addlocprlemlt  7493  addlocprlemgt  7496  addlocprlem  7497  addlocpr  7498  nqprxx  7508  ltnqex  7511  addnqprlemfl  7521  addnqprlemfu  7522  appdivnq  7525  prmuloclemcalc  7527  prmuloc  7528  mullocprlem  7532  mulnqprlemfl  7537  mulnqprlemfu  7538  ltprordil  7551  ltnqpri  7556  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  ltexpri  7575  lteupri  7579  ltaprlem  7580  recexprlemell  7584  recexprlemelu  7585  recexprlemloc  7593  recexprlempr  7594  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1u  7598  aptipr  7603  cauappcvgprlemm  7607  cauappcvgprlemlol  7609  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlem1  7621  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemlol  7632  caucvgprlemladdfu  7639  caucvgprprlemloccalc  7646  caucvgprprlemnkltj  7651  caucvgprprlemnbj  7655  caucvgprprlemml  7656  caucvgprprlemlol  7660  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  suplocexprlemss  7677  suplocexprlemru  7681  suplocexprlemlub  7686  ltsrprg  7709  caucvgsrlemasr  7752  suplocsrlemb  7768  suplocsrlem  7770  suplocsr  7771  axcaucvglemcau  7860  axpre-suploclemres  7863  negf1o  8301  apreap  8506  apreim  8522  msqge0  8535  mulge0  8538  apti  8541  apsscn  8566  mulap0bad  8577  divadddivap  8644  recnz  9305  lbzbi  9575  xadd4d  9842  ixxss1  9861  ixxss2  9862  ixxss12  9863  iccss2  9901  iccssioo2  9903  iccssico2  9904  iccen  9963  elfzole1  10111  ioom  10217  elicore  10223  flqle  10234  flqltnz  10243  addmodlteq  10354  expclzap  10501  hashennnuni  10713  zfz1isolem1  10775  recl  10817  cvg1nlemcau  10948  cvg1nlemres  10949  resqrtth  10995  fimaxre2  11190  climcl  11245  reccn2ap  11276  nnf1o  11339  summodclem3  11343  sumpr  11376  fsump1i  11396  fisumcom2  11401  fsum00  11425  fsumparts  11433  mertenslemi1  11498  prodmodclem3  11538  fprodcom2fi  11589  addsin  11705  subsin  11706  addcos  11709  subcos  11710  sinbnd2  11717  cosbnd2  11718  sin01gt0  11724  cos01gt0  11725  divgcdz  11926  divgcdnn  11930  gcdaddm  11939  bezoutlemstep  11952  dvdsgcdb  11968  dfgcd2  11969  mulgcd  11971  gcdzeq  11977  dvdsmulgcd  11980  sqgcd  11984  bezoutr  11987  lcmval  12017  lcmcllem  12021  gcddvdslcm  12027  lcmgcdlem  12031  lcmgcd  12032  lcmgcdeq  12037  lcmdvdsb  12038  mulgcddvds  12048  rpmulgcd2  12049  qredeu  12051  rpdvds  12053  isprm3  12072  divgcdodd  12097  coprm  12098  rpexp  12107  sqrt2irr  12116  qnumcl  12142  qnumdencoprm  12147  divnumden  12150  numsq  12157  phimullem  12179  eulerthlem1  12181  prmdiveq  12190  prmdivdiv  12191  hashgcdlem  12192  odzcl  12197  reumodprminv  12207  pythagtriplem19  12236  pclemub  12241  pcprendvds  12244  pcprendvds2  12245  pcpre1  12246  pcpremul  12247  pceulem  12248  pceu  12249  pczpre  12251  pczcl  12252  pcgcd1  12281  pc2dvds  12283  pcaddlem  12292  pcmpt  12295  pockthlem  12308  prmunb  12314  4sqlem7  12336  4sqlem8  12337  4sqlem9  12338  4sqlem10  12339  ennnfonelemg  12358  ennnfonelemf1  12373  ctiunctlemu1st  12389  nninfdclemf  12404  nninfdclemp1  12405  mgmidcl  12632  mndlid  12671  uniopn  12793  restbasg  12962  cntop1  12995  cnf  12998  cnpf2  13001  lmtopcnp  13044  psmetdmdm  13118  psmetf  13119  psmet0  13121  xmetf  13144  metf  13145  blhalf  13202  xmetxpbl  13302  ioo2bl  13337  tgioo  13340  cncff  13358  rescncf  13362  cdivcncfap  13381  cnopnap  13388  dedekindeulemeu  13394  dedekindicclemeu  13403  ivthinclemlm  13406  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthinclemdisj  13412  ivthdec  13416  limcimolemlt  13427  limcimo  13428  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  limccoap  13441  eldvap  13445  dvbsssg  13449  dvfgg  13451  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcj  13467  dvfre  13468  dvrecap  13471  sin0pilem1  13496  sin0pilem2  13497  pilem3  13498  tanrpcl  13552  tangtx  13553  lgsne0  13733  2sqlem8a  13752  2sqlem8  13753  nninfalllem1  14041  iooref1o  14066  alsi1d  14110  alsc1d  14112