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  simplld  528  simplrd  530  simprld  532  simp1  1024  eldifad  3212  unssad  3386  opth1  4334  opth  4335  0nelop  4346  epelg  4393  poirr  4410  brrelex1  4771  brrelex  4772  asymref  5129  soirri  5138  sotri  5139  ffdmd  5514  fcnvres  5528  fun11iun  5613  funopsn  5838  elmpocl1  6228  f1od  6236  f1o2d  6238  oprssdmm  6343  elmpom  6412  fczsupp0  6437  smoiso  6511  tfrlem1  6517  swoer  6773  ecopovtrn  6844  ecopovtrng  6847  elmapssres  6885  pmresg  6888  mapsspm  6894  en1uniel  7021  pw2f1odc  7064  xpf1o  7073  sbthlemi9  7207  supelti  7244  supsnti  7247  supisoti  7252  ctssdccl  7353  ctfoex  7360  fodjum  7388  en2eleq  7449  djuen  7469  pw1if  7486  dftap2  7513  2omotaplemst  7520  exmidapne  7522  ccfunen  7526  dfplpq2  7617  ltbtwnnqq  7678  enq0tr  7697  elnp1st2nd  7739  prcdnql  7747  prnminu  7752  prloc  7754  genpcdl  7782  addnqprulem  7791  addlocprlemlt  7794  addlocprlemgt  7797  addlocprlem  7798  addlocpr  7799  nqprxx  7809  ltnqex  7812  addnqprlemfl  7822  addnqprlemfu  7823  appdivnq  7826  prmuloclemcalc  7828  prmuloc  7829  mullocprlem  7833  mulnqprlemfl  7838  mulnqprlemfu  7839  ltprordil  7852  ltnqpri  7857  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  ltexpri  7876  lteupri  7880  ltaprlem  7881  recexprlemell  7885  recexprlemelu  7886  recexprlemloc  7894  recexprlempr  7895  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1u  7899  aptipr  7904  cauappcvgprlemm  7908  cauappcvgprlemlol  7910  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlem1  7922  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemlol  7933  caucvgprlemladdfu  7940  caucvgprprlemloccalc  7947  caucvgprprlemnkltj  7952  caucvgprprlemnbj  7956  caucvgprprlemml  7957  caucvgprprlemlol  7961  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  suplocexprlemss  7978  suplocexprlemru  7982  suplocexprlemlub  7987  ltsrprg  8010  caucvgsrlemasr  8053  suplocsrlemb  8069  suplocsrlem  8071  suplocsr  8072  axcaucvglemcau  8161  axpre-suploclemres  8164  negf1o  8603  apreap  8809  apreim  8825  msqge0  8838  mulge0  8841  apti  8844  apsscn  8869  mulap0bad  8881  divadddivap  8949  recnz  9617  lbzbi  9894  xadd4d  10164  ixxss1  10183  ixxss2  10184  ixxss12  10185  iccss2  10223  iccssioo2  10225  iccssico2  10226  iccen  10286  elfzole1  10436  ioom  10566  elicore  10572  flqle  10584  flqltnz  10593  addmodlteq  10706  expclzap  10872  hashennnuni  11087  zfz1isolem1  11150  hashdmprop2dom  11154  swrdsbslen  11296  ccatswrd  11300  ccatpfx  11331  recl  11476  cvg1nlemcau  11607  cvg1nlemres  11608  resqrtth  11654  fimaxre2  11850  climcl  11905  reccn2ap  11936  nnf1o  12000  summodclem3  12004  sumpr  12037  fsump1i  12057  fisumcom2  12062  fsum00  12086  fsumparts  12094  mertenslemi1  12159  prodmodclem3  12199  fprodcom2fi  12250  addsin  12366  subsin  12367  addcos  12370  subcos  12371  sinbnd2  12378  cosbnd2  12379  sin01gt0  12386  cos01gt0  12387  divgcdz  12605  divgcdnn  12609  gcdaddm  12618  bezoutlemstep  12631  dvdsgcdb  12647  dfgcd2  12648  mulgcd  12650  gcdzeq  12656  dvdsmulgcd  12659  sqgcd  12663  bezoutr  12666  lcmval  12698  lcmcllem  12702  gcddvdslcm  12708  lcmgcdlem  12712  lcmgcd  12713  lcmgcdeq  12718  lcmdvdsb  12719  mulgcddvds  12729  rpmulgcd2  12730  qredeu  12732  rpdvds  12734  isprm3  12753  divgcdodd  12778  coprm  12779  rpexp  12788  sqrt2irr  12797  qnumcl  12823  qnumdencoprm  12828  divnumden  12831  numsq  12838  phimullem  12860  eulerthlem1  12862  prmdiveq  12871  prmdivdiv  12872  hashgcdlem  12873  odzcl  12879  reumodprminv  12889  pythagtriplem19  12918  pclemub  12923  pcprendvds  12926  pcprendvds2  12927  pcpre1  12928  pcpremul  12929  pceulem  12930  pceu  12931  pczpre  12933  pczcl  12934  pcgcd1  12964  pc2dvds  12966  pcaddlem  12975  pcmpt  12979  pockthlem  12992  prmunb  12998  4sqlem7  13020  4sqlem8  13021  4sqlem9  13022  4sqlem10  13023  4sqlem14  13040  4sqlem15  13041  4sqlem16  13042  4sqlem17  13043  4sqlem18  13044  ennnfonelemg  13087  ennnfonelemf1  13102  ctiunctlemu1st  13118  nninfdclemf  13133  nninfdclemp1  13134  mgmidcl  13524  gsumfzval  13537  gsumval2  13543  mndlid  13581  prdsmndd  13594  imasmndf1  13600  dfgrp3mlem  13744  grplactf1o  13749  prdsgrpd  13755  prdsinvgd  13756  imasgrpf1  13762  subgsubm  13846  qusgrp  13882  ghmgrp1  13895  ghmf  13897  ghmnsgpreima  13919  kerf1ghm  13924  conjsubg  13927  gsumsplit0  13996  imasrng  14033  srgdilem  14046  srgdi  14051  srglidm  14056  ringdilem  14089  ringdi  14095  ringlidm  14100  imasring  14141  imasringf1  14142  dvdsrcld  14175  unitcld  14186  unitmulcl  14191  unitnegcl  14208  rhmghm  14240  elrhmunit  14255  subrgss  14300  subrgrcl  14304  rrgsupp  14344  lmodvscl  14384  lmodvsdi  14390  lmodvsdir  14391  lsslsp  14508  qusring  14606  crngridl  14609  znunit  14738  znrrg  14739  psrbaglesuppg  14751  psrbagcon  14755  psrbagconcl  14756  psrelbas  14759  psraddcl  14764  mplrcl  14778  uniopn  14795  restbasg  14962  cntop1  14995  cnf  14998  cnpf2  15001  lmtopcnp  15044  psmetdmdm  15118  psmetf  15119  psmet0  15121  xmetf  15144  metf  15145  blhalf  15202  xmetxpbl  15302  ioo2bl  15345  tgioo  15348  cncff  15371  rescncf  15375  cdivcncfap  15398  cnopnap  15405  divcncfap  15408  dedekindeulemeu  15416  dedekindicclemeu  15425  ivthinclemlm  15428  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthinclemdisj  15434  ivthdec  15438  ivthreinc  15439  limcimolemlt  15458  limcimo  15459  limccnpcntop  15469  limccnp2lem  15470  limccnp2cntop  15471  limccoap  15472  eldvap  15476  dvbsssg  15480  dvfgg  15482  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcj  15503  dvfre  15504  dvrecap  15507  plyco  15553  plycj  15555  sin0pilem1  15575  sin0pilem2  15576  pilem3  15577  tanrpcl  15631  tangtx  15632  perfect  15798  lgsne0  15840  lgseisen  15876  lgsquad2lem2  15884  2sqlem8a  15924  2sqlem8  15925  structgrssvtx  15966  edguhgr  16061  umgrpredgv  16071  umgrnloop2  16075  umgr2edg  16131  subuhgr  16196  subumgr  16198  subusgr  16199  wlkpropg  16248  wlkv  16250  wlkvtxeledgg  16268  wlkvtxiedgg  16270  wlk1walkdom  16283  trlsv  16308  clwwlksswrd  16321  clwwlkclwwlkn  16333  eupthv  16370  eupthseg  16376  eupth2lem3lem3fi  16394  eupth2lem3lem4fi  16397  eupth2lemsfi  16402  eulerpathprum  16404  nninfalllem1  16717  iooref1o  16749  gfsumval  16792  alsi1d  16807  alsc1d  16809