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  3222  unssad  3396  opth1  4352  opth  4353  0nelop  4364  epelg  4411  poirr  4428  brrelex1  4789  brrelex  4790  asymref  5148  soirri  5157  sotri  5158  ffdmd  5534  fcnvres  5550  fun11iun  5635  funopsn  5860  elmpocl1  6250  f1od  6258  f1o2d  6260  oprssdmm  6365  elmpom  6434  fczsupp0  6459  smoiso  6533  tfrlem1  6539  swoer  6795  ecopovtrn  6866  ecopovtrng  6869  elmapssres  6907  pmresg  6910  mapsspm  6916  en1uniel  7044  pw2f1odc  7088  xpf1o  7097  sbthlemi9  7235  fsuppfund  7247  supelti  7293  supsnti  7296  supisoti  7301  ctssdccl  7402  ctfoex  7409  fodjum  7437  en2eleq  7498  djuen  7518  pw1if  7535  dftap2  7565  2omotaplemst  7572  exmidapne  7574  ccfunen  7578  dfplpq2  7669  ltbtwnnqq  7730  enq0tr  7749  elnp1st2nd  7791  prcdnql  7799  prnminu  7804  prloc  7806  genpcdl  7834  addnqprulem  7843  addlocprlemlt  7846  addlocprlemgt  7849  addlocprlem  7850  addlocpr  7851  nqprxx  7861  ltnqex  7864  addnqprlemfl  7874  addnqprlemfu  7875  appdivnq  7878  prmuloclemcalc  7880  prmuloc  7881  mullocprlem  7885  mulnqprlemfl  7890  mulnqprlemfu  7891  ltprordil  7904  ltnqpri  7909  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  ltexpri  7928  lteupri  7932  ltaprlem  7933  recexprlemell  7937  recexprlemelu  7938  recexprlemloc  7946  recexprlempr  7947  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1u  7951  aptipr  7956  cauappcvgprlemm  7960  cauappcvgprlemlol  7962  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  cauappcvgprlem1  7974  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemlol  7985  caucvgprlemladdfu  7992  caucvgprprlemloccalc  7999  caucvgprprlemnkltj  8004  caucvgprprlemnbj  8008  caucvgprprlemml  8009  caucvgprprlemlol  8013  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  suplocexprlemss  8030  suplocexprlemru  8034  suplocexprlemlub  8039  ltsrprg  8062  caucvgsrlemasr  8105  suplocsrlemb  8121  suplocsrlem  8123  suplocsr  8124  axcaucvglemcau  8213  axpre-suploclemres  8216  negf1o  8655  apreap  8861  apreim  8877  msqge0  8890  mulge0  8893  apti  8896  apsscn  8921  mulap0bad  8933  divadddivap  9001  recnz  9671  lbzbi  9948  xadd4d  10218  ixxss1  10237  ixxss2  10238  ixxss12  10239  iccss2  10277  iccssioo2  10279  iccssico2  10280  iccen  10340  elfzole1  10490  ioom  10620  elicore  10626  flqle  10638  flqltnz  10647  addmodlteq  10760  expclzap  10926  hashennnuni  11142  zfz1isolem1  11212  hashdmprop2dom  11216  swrdsbslen  11358  ccatswrd  11362  ccatpfx  11393  recl  11538  cvg1nlemcau  11669  cvg1nlemres  11670  resqrtth  11716  fimaxre2  11912  climcl  11967  reccn2ap  11998  nnf1o  12062  summodclem3  12066  sumpr  12099  fsump1i  12119  fisumcom2  12124  fsum00  12148  fsumparts  12156  mertenslemi1  12221  prodmodclem3  12261  fprodcom2fi  12312  addsin  12428  subsin  12429  addcos  12432  subcos  12433  sinbnd2  12440  cosbnd2  12441  sin01gt0  12448  cos01gt0  12449  divgcdz  12667  divgcdnn  12671  gcdaddm  12680  bezoutlemstep  12693  dvdsgcdb  12709  dfgcd2  12710  mulgcd  12712  gcdzeq  12718  dvdsmulgcd  12721  sqgcd  12725  bezoutr  12728  lcmval  12760  lcmcllem  12764  gcddvdslcm  12770  lcmgcdlem  12774  lcmgcd  12775  lcmgcdeq  12780  lcmdvdsb  12781  mulgcddvds  12791  rpmulgcd2  12792  qredeu  12794  rpdvds  12796  isprm3  12815  divgcdodd  12840  coprm  12841  rpexp  12850  sqrt2irr  12859  qnumcl  12885  qnumdencoprm  12890  divnumden  12893  numsq  12900  phimullem  12922  eulerthlem1  12924  prmdiveq  12933  prmdivdiv  12934  hashgcdlem  12935  odzcl  12941  reumodprminv  12951  pythagtriplem19  12980  pclemub  12985  pcprendvds  12988  pcprendvds2  12989  pcpre1  12990  pcpremul  12991  pceulem  12992  pceu  12993  pczpre  12995  pczcl  12996  pcgcd1  13026  pc2dvds  13028  pcaddlem  13037  pcmpt  13041  pockthlem  13054  prmunb  13060  4sqlem7  13082  4sqlem8  13083  4sqlem9  13084  4sqlem10  13085  4sqlem14  13102  4sqlem15  13103  4sqlem16  13104  4sqlem17  13105  4sqlem18  13106  ballotfilem2  13142  ennnfonelemg  13154  ennnfonelemf1  13169  ctiunctlemu1st  13185  nninfdclemf  13200  nninfdclemp1  13201  mgmidcl  13591  gsumfzval  13604  gsumval2  13610  mndlid  13648  prdsmndd  13661  imasmndf1  13667  dfgrp3mlem  13811  grplactf1o  13816  prdsgrpd  13822  prdsinvgd  13823  imasgrpf1  13829  subgsubm  13913  qusgrp  13949  ghmgrp1  13962  ghmf  13964  ghmnsgpreima  13986  kerf1ghm  13991  conjsubg  13994  gsumsplit0  14063  imasrng  14100  srgdilem  14113  srgdi  14118  srglidm  14123  ringdilem  14156  ringdi  14162  ringlidm  14167  imasring  14208  imasringf1  14209  dvdsrcld  14242  unitcld  14253  unitmulcl  14258  unitnegcl  14275  rhmghm  14307  elrhmunit  14322  subrgss  14367  subrgrcl  14371  rrgsupp  14411  lmodvscl  14453  lmodvsdi  14459  lmodvsdir  14460  lsslsp  14577  qusring  14675  crngridl  14678  znunit  14807  znrrg  14808  psrbaglesuppg  14821  psrbagcon  14826  psrbagconcl  14827  psrelbas  14830  psraddcl  14835  mplrcl  14849  uniopn  14866  restbasg  15033  cntop1  15066  cnf  15069  cnpf2  15072  lmtopcnp  15115  psmetdmdm  15189  psmetf  15190  psmet0  15192  xmetf  15215  metf  15216  blhalf  15273  xmetxpbl  15373  ioo2bl  15416  tgioo  15419  cncff  15442  rescncf  15446  cdivcncfap  15469  cnopnap  15476  divcncfap  15479  dedekindeulemeu  15487  dedekindicclemeu  15496  ivthinclemlm  15499  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthinclemdisj  15505  ivthdec  15509  ivthreinc  15510  limcimolemlt  15529  limcimo  15530  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  limccoap  15543  eldvap  15547  dvbsssg  15551  dvfgg  15553  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcj  15574  dvfre  15575  dvrecap  15578  plyco  15624  plycj  15626  sin0pilem1  15646  sin0pilem2  15647  pilem3  15648  tanrpcl  15702  tangtx  15703  perfect  15869  lgsne0  15911  lgseisen  15947  lgsquad2lem2  15955  2sqlem8a  15995  2sqlem8  15996  structgrssvtx  16037  edguhgr  16132  umgrpredgv  16142  umgrnloop2  16146  umgr2edg  16202  subuhgr  16267  subumgr  16269  subusgr  16270  wlkpropg  16319  wlkv  16321  wlkvtxeledgg  16339  wlkvtxiedgg  16341  wlk1walkdom  16354  trlsv  16379  clwwlksswrd  16392  clwwlkclwwlkn  16404  eupthv  16441  eupthseg  16447  eupth2lem3lem3fi  16465  eupth2lem3lem4fi  16468  eupth2lemsfi  16473  eulerpathprum  16475  nninfalllem1  16786  iooref1o  16818  gfsumval  16862  alsi1d  16878  alsc1d  16880