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  1021  eldifad  3208  unssad  3381  opth1  4322  opth  4323  0nelop  4334  epelg  4381  poirr  4398  brrelex1  4758  brrelex  4759  asymref  5114  soirri  5123  sotri  5124  ffdmd  5497  fcnvres  5511  fun11iun  5595  funopsn  5819  elmpocl1  6207  f1od  6215  f1o2d  6217  oprssdmm  6323  smoiso  6454  tfrlem1  6460  swoer  6716  ecopovtrn  6787  ecopovtrng  6790  elmapssres  6828  pmresg  6831  mapsspm  6837  en1uniel  6964  pw2f1odc  7004  xpf1o  7013  sbthlemi9  7143  supelti  7180  supsnti  7183  supisoti  7188  ctssdccl  7289  ctfoex  7296  fodjum  7324  en2eleq  7384  djuen  7404  pw1if  7421  dftap2  7448  2omotaplemst  7455  exmidapne  7457  ccfunen  7461  dfplpq2  7552  ltbtwnnqq  7613  enq0tr  7632  elnp1st2nd  7674  prcdnql  7682  prnminu  7687  prloc  7689  genpcdl  7717  addnqprulem  7726  addlocprlemlt  7729  addlocprlemgt  7732  addlocprlem  7733  addlocpr  7734  nqprxx  7744  ltnqex  7747  addnqprlemfl  7757  addnqprlemfu  7758  appdivnq  7761  prmuloclemcalc  7763  prmuloc  7764  mullocprlem  7768  mulnqprlemfl  7773  mulnqprlemfu  7774  ltprordil  7787  ltnqpri  7792  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  ltexpri  7811  lteupri  7815  ltaprlem  7816  recexprlemell  7820  recexprlemelu  7821  recexprlemloc  7829  recexprlempr  7830  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1u  7834  aptipr  7839  cauappcvgprlemm  7843  cauappcvgprlemlol  7845  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlem1  7857  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemlol  7868  caucvgprlemladdfu  7875  caucvgprprlemloccalc  7882  caucvgprprlemnkltj  7887  caucvgprprlemnbj  7891  caucvgprprlemml  7892  caucvgprprlemlol  7896  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  suplocexprlemss  7913  suplocexprlemru  7917  suplocexprlemlub  7922  ltsrprg  7945  caucvgsrlemasr  7988  suplocsrlemb  8004  suplocsrlem  8006  suplocsr  8007  axcaucvglemcau  8096  axpre-suploclemres  8099  negf1o  8539  apreap  8745  apreim  8761  msqge0  8774  mulge0  8777  apti  8780  apsscn  8805  mulap0bad  8817  divadddivap  8885  recnz  9551  lbzbi  9823  xadd4d  10093  ixxss1  10112  ixxss2  10113  ixxss12  10114  iccss2  10152  iccssioo2  10154  iccssico2  10155  iccen  10214  elfzole1  10364  ioom  10492  elicore  10498  flqle  10510  flqltnz  10519  addmodlteq  10632  expclzap  10798  hashennnuni  11013  zfz1isolem1  11075  hashdmprop2dom  11079  swrdsbslen  11213  ccatswrd  11217  ccatpfx  11248  recl  11379  cvg1nlemcau  11510  cvg1nlemres  11511  resqrtth  11557  fimaxre2  11753  climcl  11808  reccn2ap  11839  nnf1o  11902  summodclem3  11906  sumpr  11939  fsump1i  11959  fisumcom2  11964  fsum00  11988  fsumparts  11996  mertenslemi1  12061  prodmodclem3  12101  fprodcom2fi  12152  addsin  12268  subsin  12269  addcos  12272  subcos  12273  sinbnd2  12280  cosbnd2  12281  sin01gt0  12288  cos01gt0  12289  divgcdz  12507  divgcdnn  12511  gcdaddm  12520  bezoutlemstep  12533  dvdsgcdb  12549  dfgcd2  12550  mulgcd  12552  gcdzeq  12558  dvdsmulgcd  12561  sqgcd  12565  bezoutr  12568  lcmval  12600  lcmcllem  12604  gcddvdslcm  12610  lcmgcdlem  12614  lcmgcd  12615  lcmgcdeq  12620  lcmdvdsb  12621  mulgcddvds  12631  rpmulgcd2  12632  qredeu  12634  rpdvds  12636  isprm3  12655  divgcdodd  12680  coprm  12681  rpexp  12690  sqrt2irr  12699  qnumcl  12725  qnumdencoprm  12730  divnumden  12733  numsq  12740  phimullem  12762  eulerthlem1  12764  prmdiveq  12773  prmdivdiv  12774  hashgcdlem  12775  odzcl  12781  reumodprminv  12791  pythagtriplem19  12820  pclemub  12825  pcprendvds  12828  pcprendvds2  12829  pcpre1  12830  pcpremul  12831  pceulem  12832  pceu  12833  pczpre  12835  pczcl  12836  pcgcd1  12866  pc2dvds  12868  pcaddlem  12877  pcmpt  12881  pockthlem  12894  prmunb  12900  4sqlem7  12922  4sqlem8  12923  4sqlem9  12924  4sqlem10  12925  4sqlem14  12942  4sqlem15  12943  4sqlem16  12944  4sqlem17  12945  4sqlem18  12946  ennnfonelemg  12989  ennnfonelemf1  13004  ctiunctlemu1st  13020  nninfdclemf  13035  nninfdclemp1  13036  mgmidcl  13426  gsumfzval  13439  gsumval2  13445  mndlid  13483  prdsmndd  13496  imasmndf1  13502  dfgrp3mlem  13646  grplactf1o  13651  prdsgrpd  13657  prdsinvgd  13658  imasgrpf1  13664  subgsubm  13748  qusgrp  13784  ghmgrp1  13797  ghmf  13799  ghmnsgpreima  13821  kerf1ghm  13826  conjsubg  13829  imasrng  13934  srgdilem  13947  srgdi  13952  srglidm  13957  ringdilem  13990  ringdi  13996  ringlidm  14001  imasring  14042  imasringf1  14043  dvdsrcld  14076  unitcld  14087  unitmulcl  14092  unitnegcl  14109  rhmghm  14141  elrhmunit  14156  subrgss  14201  subrgrcl  14205  lmodvscl  14284  lmodvsdi  14290  lmodvsdir  14291  lsslsp  14408  qusring  14506  crngridl  14509  znunit  14638  znrrg  14639  psrbaglesuppg  14651  psrelbas  14654  psraddcl  14659  mplrcl  14673  uniopn  14690  restbasg  14857  cntop1  14890  cnf  14893  cnpf2  14896  lmtopcnp  14939  psmetdmdm  15013  psmetf  15014  psmet0  15016  xmetf  15039  metf  15040  blhalf  15097  xmetxpbl  15197  ioo2bl  15240  tgioo  15243  cncff  15266  rescncf  15270  cdivcncfap  15293  cnopnap  15300  divcncfap  15303  dedekindeulemeu  15311  dedekindicclemeu  15320  ivthinclemlm  15323  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthinclemdisj  15329  ivthdec  15333  ivthreinc  15334  limcimolemlt  15353  limcimo  15354  limccnpcntop  15364  limccnp2lem  15365  limccnp2cntop  15366  limccoap  15367  eldvap  15371  dvbsssg  15375  dvfgg  15377  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcj  15398  dvfre  15399  dvrecap  15402  plyco  15448  plycj  15450  sin0pilem1  15470  sin0pilem2  15471  pilem3  15472  tanrpcl  15526  tangtx  15527  perfect  15690  lgsne0  15732  lgseisen  15768  lgsquad2lem2  15776  2sqlem8a  15816  2sqlem8  15817  structgrssvtx  15858  edguhgr  15950  umgrpredgv  15960  umgrnloop2  15964  umgr2edg  16020  wlkpropg  16065  wlkv  16067  wlkvtxeledgg  16085  wlkvtxiedgg  16087  wlk1walkdom  16100  trlsv  16123  clwwlksswrd  16135  nninfalllem1  16434  iooref1o  16462  alsi1d  16509  alsc1d  16511