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  999  eldifad  3176  unssad  3349  opth1  4279  opth  4280  0nelop  4291  epelg  4336  poirr  4353  brrelex1  4713  brrelex  4714  asymref  5067  soirri  5076  sotri  5077  fcnvres  5458  fun11iun  5542  funopsn  5761  elmpocl1  6141  f1od  6148  f1o2d  6150  oprssdmm  6256  smoiso  6387  tfrlem1  6393  swoer  6647  ecopovtrn  6718  ecopovtrng  6721  elmapssres  6759  pmresg  6762  mapsspm  6768  en1uniel  6895  pw2f1odc  6931  xpf1o  6940  sbthlemi9  7066  supelti  7103  supsnti  7106  supisoti  7111  ctssdccl  7212  ctfoex  7219  fodjum  7247  en2eleq  7302  djuen  7322  dftap2  7362  2omotaplemst  7369  exmidapne  7371  ccfunen  7375  dfplpq2  7466  ltbtwnnqq  7527  enq0tr  7546  elnp1st2nd  7588  prcdnql  7596  prnminu  7601  prloc  7603  genpcdl  7631  addnqprulem  7640  addlocprlemlt  7643  addlocprlemgt  7646  addlocprlem  7647  addlocpr  7648  nqprxx  7658  ltnqex  7661  addnqprlemfl  7671  addnqprlemfu  7672  appdivnq  7675  prmuloclemcalc  7677  prmuloc  7678  mullocprlem  7682  mulnqprlemfl  7687  mulnqprlemfu  7688  ltprordil  7701  ltnqpri  7706  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  ltexprlemdisj  7718  ltexprlemloc  7719  ltexprlemfl  7721  ltexprlemrl  7722  ltexprlemfu  7723  ltexprlemru  7724  ltexpri  7725  lteupri  7729  ltaprlem  7730  recexprlemell  7734  recexprlemelu  7735  recexprlemloc  7743  recexprlempr  7744  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1u  7748  aptipr  7753  cauappcvgprlemm  7757  cauappcvgprlemlol  7759  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlem1  7771  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemlol  7782  caucvgprlemladdfu  7789  caucvgprprlemloccalc  7796  caucvgprprlemnkltj  7801  caucvgprprlemnbj  7805  caucvgprprlemml  7806  caucvgprprlemlol  7810  caucvgprprlemloc  7815  caucvgprprlemexbt  7818  suplocexprlemss  7827  suplocexprlemru  7831  suplocexprlemlub  7836  ltsrprg  7859  caucvgsrlemasr  7902  suplocsrlemb  7918  suplocsrlem  7920  suplocsr  7921  axcaucvglemcau  8010  axpre-suploclemres  8013  negf1o  8453  apreap  8659  apreim  8675  msqge0  8688  mulge0  8691  apti  8694  apsscn  8719  mulap0bad  8731  divadddivap  8799  recnz  9465  lbzbi  9736  xadd4d  10006  ixxss1  10025  ixxss2  10026  ixxss12  10027  iccss2  10065  iccssioo2  10067  iccssico2  10068  iccen  10127  elfzole1  10277  ioom  10401  elicore  10407  flqle  10419  flqltnz  10428  addmodlteq  10541  expclzap  10707  hashennnuni  10922  zfz1isolem1  10983  hashdmprop2dom  10987  recl  11135  cvg1nlemcau  11266  cvg1nlemres  11267  resqrtth  11313  fimaxre2  11509  climcl  11564  reccn2ap  11595  nnf1o  11658  summodclem3  11662  sumpr  11695  fsump1i  11715  fisumcom2  11720  fsum00  11744  fsumparts  11752  mertenslemi1  11817  prodmodclem3  11857  fprodcom2fi  11908  addsin  12024  subsin  12025  addcos  12028  subcos  12029  sinbnd2  12036  cosbnd2  12037  sin01gt0  12044  cos01gt0  12045  divgcdz  12263  divgcdnn  12267  gcdaddm  12276  bezoutlemstep  12289  dvdsgcdb  12305  dfgcd2  12306  mulgcd  12308  gcdzeq  12314  dvdsmulgcd  12317  sqgcd  12321  bezoutr  12324  lcmval  12356  lcmcllem  12360  gcddvdslcm  12366  lcmgcdlem  12370  lcmgcd  12371  lcmgcdeq  12376  lcmdvdsb  12377  mulgcddvds  12387  rpmulgcd2  12388  qredeu  12390  rpdvds  12392  isprm3  12411  divgcdodd  12436  coprm  12437  rpexp  12446  sqrt2irr  12455  qnumcl  12481  qnumdencoprm  12486  divnumden  12489  numsq  12496  phimullem  12518  eulerthlem1  12520  prmdiveq  12529  prmdivdiv  12530  hashgcdlem  12531  odzcl  12537  reumodprminv  12547  pythagtriplem19  12576  pclemub  12581  pcprendvds  12584  pcprendvds2  12585  pcpre1  12586  pcpremul  12587  pceulem  12588  pceu  12589  pczpre  12591  pczcl  12592  pcgcd1  12622  pc2dvds  12624  pcaddlem  12633  pcmpt  12637  pockthlem  12650  prmunb  12656  4sqlem7  12678  4sqlem8  12679  4sqlem9  12680  4sqlem10  12681  4sqlem14  12698  4sqlem15  12699  4sqlem16  12700  4sqlem17  12701  4sqlem18  12702  ennnfonelemg  12745  ennnfonelemf1  12760  ctiunctlemu1st  12776  nninfdclemf  12791  nninfdclemp1  12792  mgmidcl  13181  gsumfzval  13194  gsumval2  13200  mndlid  13238  prdsmndd  13251  imasmndf1  13257  dfgrp3mlem  13401  grplactf1o  13406  prdsgrpd  13412  prdsinvgd  13413  imasgrpf1  13419  subgsubm  13503  qusgrp  13539  ghmgrp1  13552  ghmf  13554  ghmnsgpreima  13576  kerf1ghm  13581  conjsubg  13584  imasrng  13689  srgdilem  13702  srgdi  13707  srglidm  13712  ringdilem  13745  ringdi  13751  ringlidm  13756  imasring  13797  imasringf1  13798  dvdsrcld  13830  unitcld  13841  unitmulcl  13846  unitnegcl  13863  rhmghm  13895  elrhmunit  13910  subrgss  13955  subrgrcl  13959  lmodvscl  14038  lmodvsdi  14044  lmodvsdir  14045  lsslsp  14162  qusring  14260  crngridl  14263  znunit  14392  znrrg  14393  psrbaglesuppg  14405  psrelbas  14408  psraddcl  14413  mplrcl  14427  uniopn  14444  restbasg  14611  cntop1  14644  cnf  14647  cnpf2  14650  lmtopcnp  14693  psmetdmdm  14767  psmetf  14768  psmet0  14770  xmetf  14793  metf  14794  blhalf  14851  xmetxpbl  14951  ioo2bl  14994  tgioo  14997  cncff  15020  rescncf  15024  cdivcncfap  15047  cnopnap  15054  divcncfap  15057  dedekindeulemeu  15065  dedekindicclemeu  15074  ivthinclemlm  15077  ivthinclemlopn  15079  ivthinclemuopn  15081  ivthinclemdisj  15083  ivthdec  15087  ivthreinc  15088  limcimolemlt  15107  limcimo  15108  limccnpcntop  15118  limccnp2lem  15119  limccnp2cntop  15120  limccoap  15121  eldvap  15125  dvbsssg  15129  dvfgg  15131  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcj  15152  dvfre  15153  dvrecap  15156  plyco  15202  plycj  15204  sin0pilem1  15224  sin0pilem2  15225  pilem3  15226  tanrpcl  15280  tangtx  15281  perfect  15444  lgsne0  15486  lgseisen  15522  lgsquad2lem2  15530  2sqlem8a  15570  2sqlem8  15571  structgrssvtx  15610  nninfalllem1  15907  iooref1o  15935  alsi1d  15982  alsc1d  15984