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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is used by:  biimp  118  simplbi  274  simprbda  383  simplld  532  simplrd  534  simprld  536  simp1  1028  eldifad  3231  unssad  3406  opth1  4376  opth  4377  0nelop  4388  epelg  4435  poirr  4452  brrelex1  4814  brrelex  4815  asymref  5173  soirri  5182  sotri  5183  ffdmd  5559  fcnvres  5575  fun11iun  5660  funopsn  5891  elmpocl1  6285  f1od  6293  f1o2d  6295  oprssdmm  6405  elmpom  6474  fczsupp0  6499  smoiso  6573  tfrlem1  6579  swoer  6835  ecopovtrn  6906  ecopovtrng  6909  elmapssres  6954  pmresg  6957  mapsspm  6963  en1uniel  7091  pw2f1odc  7135  xpf1o  7144  sbthlemi9  7282  fsuppfund  7294  supelti  7343  supsnti  7346  supisoti  7351  ctssdccl  7452  ctfoex  7459  fodjum  7487  en2eleq  7548  djuen  7568  pw1if  7585  dftap2  7618  2omotaplemst  7625  exmidapne  7627  ccfunen  7631  dfplpq2  7722  ltbtwnnqq  7783  enq0tr  7802  elnp1st2nd  7844  prcdnql  7852  prnminu  7857  prloc  7859  genpcdl  7887  addnqprulem  7896  addlocprlemlt  7899  addlocprlemgt  7902  addlocprlem  7903  addlocpr  7904  nqprxx  7914  ltnqex  7917  addnqprlemfl  7927  addnqprlemfu  7928  appdivnq  7931  prmuloclemcalc  7933  prmuloc  7934  mullocprlem  7938  mulnqprlemfl  7943  mulnqprlemfu  7944  ltprordil  7957  ltnqpri  7962  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltexpri  7981  lteupri  7985  ltaprlem  7986  recexprlemell  7990  recexprlemelu  7991  recexprlemloc  7999  recexprlempr  8000  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1u  8004  aptipr  8009  cauappcvgprlemm  8013  cauappcvgprlemlol  8015  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlem1  8027  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemlol  8038  caucvgprlemladdfu  8045  caucvgprprlemloccalc  8052  caucvgprprlemnkltj  8057  caucvgprprlemnbj  8061  caucvgprprlemml  8062  caucvgprprlemlol  8066  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  suplocexprlemss  8083  suplocexprlemru  8087  suplocexprlemlub  8092  ltsrprg  8115  caucvgsrlemasr  8158  suplocsrlemb  8174  suplocsrlem  8176  suplocsr  8177  axcaucvglemcau  8266  axpre-suploclemres  8269  negf1o  8711  apreap  8918  apreim  8934  msqge0  8947  mulge0  8950  apti  8953  apsscn  8978  mulap0bad  8990  divadddivap  9060  recnz  9744  lbzbi  10026  xadd4d  10298  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iccssioo2  10359  iccssico2  10360  iccen  10420  elfzole1  10574  infssfzcldc  10680  infssfzledc  10681  ioom  10706  elicore  10712  flqle  10726  flapge  10731  flaplt  10733  flqltnz  10737  addmodlteq  10850  expclzap  11016  hashennnuni  11234  zfz1isolem1  11308  hashdmprop2dom  11312  swrdsbslen  11454  ccatswrd  11458  ccatpfx  11489  recl  11634  sq01  11676  cvg1nlemcau  11766  cvg1nlemres  11767  resqrtth  11813  fimaxre2  12010  climcl  12067  reccn2ap  12098  nnf1o  12162  summodclem3  12166  sumpr  12199  fsump1i  12219  fisumcom2  12224  fsum00  12248  fsumparts  12256  mertenslemi1  12321  prodmodclem3  12361  fprodcom2fi  12412  addsin  12528  subsin  12529  addcos  12532  subcos  12533  sinbnd2  12540  cosbnd2  12541  sin01gt0  12548  cos01gt0  12549  divgcdz  12767  divgcdnn  12771  gcdaddm  12780  bezoutlemstep  12793  dvdsgcdb  12809  dfgcd2  12810  mulgcd  12812  gcdzeq  12818  dvdsmulgcd  12821  sqgcd  12825  bezoutr  12828  lcmval  12860  lcmcllem  12864  gcddvdslcm  12870  lcmgcdlem  12874  lcmgcd  12875  lcmgcdeq  12880  lcmdvdsb  12881  mulgcddvds  12891  rpmulgcd2  12892  qredeu  12894  rpdvds  12896  isprm3  12915  divgcdodd  12941  coprm  12942  rpexp  12951  sqrt2irr  12960  qnumcl  12987  qnumdencoprm  12992  divnumden  12995  numsq  13002  phimullem  13026  eulerthlem1  13028  prmdiveq  13037  prmdivdiv  13038  hashgcdlem  13039  odzcl  13045  reumodprminv  13055  pythagtriplem19  13084  pclemub  13089  pcprendvds  13092  pcprendvds2  13093  pcpre1  13094  pcpremul  13095  pceulem  13096  pceu  13097  pczpre  13099  pczcl  13100  pcgcd1  13130  pc2dvds  13132  pcaddlem  13141  pcmpt  13145  pockthlem  13158  prmunb  13164  4sqlem7  13186  4sqlem8  13187  4sqlem9  13188  4sqlem10  13189  4sqlem14  13206  4sqlem15  13207  4sqlem16  13208  4sqlem17  13209  4sqlem18  13210  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemimin  13301  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsv  13305  ballotfilemsgt1  13306  ballotfilemsdom  13307  ballotfilemsel1i  13308  ballotfilemsf1o  13309  ballotfilemsi  13310  ballotfilemsima  13311  ballotfilemscr  13314  ballotfilemrv  13315  ballotfilemrv2  13317  ballotfilemro  13318  ballotfilemfrc  13322  ballotfilemfrci  13323  ballotfilemfrceq  13324  ballotfilemfrcn0  13325  ballotfilemrc  13326  ballotfilemirc  13327  ballotfilemrinv0  13328  ballotfilem1ri  13330  ennnfonelemg  13346  ennnfonelemf1  13361  ctiunctlemu1st  13377  nninfdclemf  13392  nninfdclemp1  13393  mgmidcl  13751  gzsumfzval  13764  gzsumval2  13767  mndlid  13801  imasmndf1  13814  dfgrp3mlem  13956  grplactf1o  13961  imasgrpf1  13968  subgsubm  14052  qusgrp  14088  ghmgrp1  14101  ghmf  14103  ghmnsgpreima  14125  kerf1ghm  14130  conjsubg  14133  resscntz  14160  gzsumsplit0  14232  gsumvalfi  14236  prdsmndd  14278  prdsgrpd  14281  prdsinvgd  14282  imasrng  14339  srgdilem  14357  srgdi  14362  srglidm  14367  ringdilem  14400  ringdi  14407  ringlidm  14412  imasring  14453  imasringf1  14454  dvdsrcld  14488  unitcld  14499  unitmulcl  14504  unitnegcl  14521  rhmghm  14553  elrhmunit  14568  subrgss  14614  subrgrcl  14618  rrgsupp  14658  lmodvscl  14725  lmodvsdi  14732  lmodvsdir  14733  lsslsp  14850  qusring  14948  crngridl  14951  znunit  15078  znrrg  15079  assaass  15088  assalmod  15090  psrbaglesuppg  15141  psrbagcon  15146  psrbagconcl  15148  psrelbas  15151  psraddcl  15156  rhmpsrfilem2  15157  psrmulfval  15159  mplrcl  15176  uniopn  15193  restbasg  15360  cntop1  15393  cnf  15396  cnpf2  15399  lmtopcnp  15442  psmetdmdm  15516  psmetf  15517  psmet0  15519  xmetf  15542  metf  15543  blhalf  15600  xmetxpbl  15700  ioo2bl  15743  tgioo  15746  cncff  15769  rescncf  15773  cdivcncfap  15796  cnopnap  15803  divcncfap  15806  dedekindeulemeu  15814  dedekindicclemeu  15823  ivthinclemlm  15826  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthinclemdisj  15832  ivthdec  15836  ivthreinc  15837  limcimolemlt  15856  limcimo  15857  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  limccoap  15870  eldvap  15874  dvbsssg  15878  dvfgg  15880  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcj  15901  dvfre  15902  dvrecap  15905  plyco  15951  plycj  15953  sin0pilem1  15974  sin0pilem2  15975  pilem3  15976  tanrpcl  16030  tangtx  16031  zprmlogbaplem2  16177  zprmlogbaplem3  16178  ppiqsval2  16202  chtqge0  16208  chtqwordi  16224  chtublem  16256  perfect  16262  bposlem1  16272  bposlem4  16275  bposlem5  16276  bposlem9  16280  lgsne0  16323  lgseisen  16359  lgsquad2lem2  16367  2sqlem8a  16407  2sqlem8  16408  structgrssvtx  16449  edguhgr  16544  umgrpredgv  16554  umgrnloop2  16558  umgr2edg  16614  subuhgr  16679  subumgr  16681  subusgr  16682  wlkpropg  16731  wlkv  16733  wlkvtxeledgg  16751  wlkvtxiedgg  16753  wlk1walkdom  16766  trlsv  16791  clwwlksswrd  16804  clwwlkclwwlkn  16816  eupthv  16853  eupthseg  16859  eupth2lem3lem3fi  16877  eupth2lem3lem4fi  16880  eupth2lemsfi  16885  eulerpathprum  16887  nninfalllem1  17217  iooref1o  17249  als1d  17300  rals1d  17302  alseu1d  17336  ralseu1d  17338