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  532  simplrd  534  simprld  536  simp1  1028  eldifad  3231  unssad  3406  opth1  4371  opth  4372  0nelop  4383  epelg  4430  poirr  4447  brrelex1  4809  brrelex  4810  asymref  5168  soirri  5177  sotri  5178  ffdmd  5554  fcnvres  5570  fun11iun  5655  funopsn  5882  elmpocl1  6275  f1od  6283  f1o2d  6285  oprssdmm  6395  elmpom  6464  fczsupp0  6489  smoiso  6563  tfrlem1  6569  swoer  6825  ecopovtrn  6896  ecopovtrng  6899  elmapssres  6944  pmresg  6947  mapsspm  6953  en1uniel  7081  pw2f1odc  7125  xpf1o  7134  sbthlemi9  7272  fsuppfund  7284  supelti  7332  supsnti  7335  supisoti  7340  ctssdccl  7441  ctfoex  7448  fodjum  7476  en2eleq  7537  djuen  7557  pw1if  7574  dftap2  7607  2omotaplemst  7614  exmidapne  7616  ccfunen  7620  dfplpq2  7711  ltbtwnnqq  7772  enq0tr  7791  elnp1st2nd  7833  prcdnql  7841  prnminu  7846  prloc  7848  genpcdl  7876  addnqprulem  7885  addlocprlemlt  7888  addlocprlemgt  7891  addlocprlem  7892  addlocpr  7893  nqprxx  7903  ltnqex  7906  addnqprlemfl  7916  addnqprlemfu  7917  appdivnq  7920  prmuloclemcalc  7922  prmuloc  7923  mullocprlem  7927  mulnqprlemfl  7932  mulnqprlemfu  7933  ltprordil  7946  ltnqpri  7951  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  ltexpri  7970  lteupri  7974  ltaprlem  7975  recexprlemell  7979  recexprlemelu  7980  recexprlemloc  7988  recexprlempr  7989  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1u  7993  aptipr  7998  cauappcvgprlemm  8002  cauappcvgprlemlol  8004  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlem1  8016  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemlol  8027  caucvgprlemladdfu  8034  caucvgprprlemloccalc  8041  caucvgprprlemnkltj  8046  caucvgprprlemnbj  8050  caucvgprprlemml  8051  caucvgprprlemlol  8055  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  suplocexprlemss  8072  suplocexprlemru  8076  suplocexprlemlub  8081  ltsrprg  8104  caucvgsrlemasr  8147  suplocsrlemb  8163  suplocsrlem  8165  suplocsr  8166  axcaucvglemcau  8255  axpre-suploclemres  8258  negf1o  8699  apreap  8905  apreim  8921  msqge0  8934  mulge0  8937  apti  8940  apsscn  8965  mulap0bad  8977  divadddivap  9047  recnz  9718  lbzbi  9995  xadd4d  10266  ixxss1  10285  ixxss2  10286  ixxss12  10287  iccss2  10325  iccssioo2  10327  iccssico2  10328  iccen  10388  elfzole1  10541  infssfzcldc  10647  infssfzledc  10648  ioom  10673  elicore  10679  flqle  10691  flqltnz  10700  addmodlteq  10813  expclzap  10979  hashennnuni  11196  zfz1isolem1  11270  hashdmprop2dom  11274  swrdsbslen  11416  ccatswrd  11420  ccatpfx  11451  recl  11596  sq01  11638  cvg1nlemcau  11728  cvg1nlemres  11729  resqrtth  11775  fimaxre2  11971  climcl  12026  reccn2ap  12057  nnf1o  12121  summodclem3  12125  sumpr  12158  fsump1i  12178  fisumcom2  12183  fsum00  12207  fsumparts  12215  mertenslemi1  12280  prodmodclem3  12320  fprodcom2fi  12371  addsin  12487  subsin  12488  addcos  12491  subcos  12492  sinbnd2  12499  cosbnd2  12500  sin01gt0  12507  cos01gt0  12508  divgcdz  12726  divgcdnn  12730  gcdaddm  12739  bezoutlemstep  12752  dvdsgcdb  12768  dfgcd2  12769  mulgcd  12771  gcdzeq  12777  dvdsmulgcd  12780  sqgcd  12784  bezoutr  12787  lcmval  12819  lcmcllem  12823  gcddvdslcm  12829  lcmgcdlem  12833  lcmgcd  12834  lcmgcdeq  12839  lcmdvdsb  12840  mulgcddvds  12850  rpmulgcd2  12851  qredeu  12853  rpdvds  12855  isprm3  12874  divgcdodd  12899  coprm  12900  rpexp  12909  sqrt2irr  12918  qnumcl  12944  qnumdencoprm  12949  divnumden  12952  numsq  12959  phimullem  12981  eulerthlem1  12983  prmdiveq  12992  prmdivdiv  12993  hashgcdlem  12994  odzcl  13000  reumodprminv  13010  pythagtriplem19  13039  pclemub  13044  pcprendvds  13047  pcprendvds2  13048  pcpre1  13049  pcpremul  13050  pceulem  13051  pceu  13052  pczpre  13054  pczcl  13055  pcgcd1  13085  pc2dvds  13087  pcaddlem  13096  pcmpt  13100  pockthlem  13113  prmunb  13119  4sqlem7  13141  4sqlem8  13142  4sqlem9  13143  4sqlem10  13144  4sqlem14  13161  4sqlem15  13162  4sqlem16  13163  4sqlem17  13164  4sqlem18  13165  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemimin  13227  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemsv  13231  ballotfilemsgt1  13232  ballotfilemsdom  13233  ballotfilemsel1i  13234  ballotfilemsf1o  13235  ballotfilemsi  13236  ballotfilemsima  13237  ballotfilemscr  13240  ballotfilemrv  13241  ballotfilemrv2  13243  ballotfilemro  13244  ballotfilemfrc  13248  ballotfilemfrci  13249  ballotfilemfrceq  13250  ballotfilemfrcn0  13251  ballotfilemrc  13252  ballotfilemirc  13253  ballotfilemrinv0  13254  ballotfilem1ri  13256  ennnfonelemg  13272  ennnfonelemf1  13287  ctiunctlemu1st  13303  nninfdclemf  13318  nninfdclemp1  13319  mgmidcl  13675  gzsumfzval  13688  gzsumval2  13691  mndlid  13725  imasmndf1  13738  dfgrp3mlem  13880  grplactf1o  13885  imasgrpf1  13892  subgsubm  13976  qusgrp  14012  ghmgrp1  14025  ghmf  14027  ghmnsgpreima  14049  kerf1ghm  14054  conjsubg  14057  gzsumsplit0  14125  gsumvalfi  14129  prdsmndd  14171  prdsgrpd  14174  prdsinvgd  14175  imasrng  14230  srgdilem  14247  srgdi  14252  srglidm  14257  ringdilem  14290  ringdi  14296  ringlidm  14301  imasring  14342  imasringf1  14343  dvdsrcld  14377  unitcld  14388  unitmulcl  14393  unitnegcl  14410  rhmghm  14442  elrhmunit  14457  subrgss  14503  subrgrcl  14507  rrgsupp  14547  lmodvscl  14614  lmodvsdi  14620  lmodvsdir  14621  lsslsp  14738  qusring  14836  crngridl  14839  znunit  14966  znrrg  14967  psrbaglesuppg  14980  psrbagcon  14985  psrbagconcl  14986  psrelbas  14989  psraddcl  14994  mplrcl  15008  uniopn  15025  restbasg  15192  cntop1  15225  cnf  15228  cnpf2  15231  lmtopcnp  15274  psmetdmdm  15348  psmetf  15349  psmet0  15351  xmetf  15374  metf  15375  blhalf  15432  xmetxpbl  15532  ioo2bl  15575  tgioo  15578  cncff  15601  rescncf  15605  cdivcncfap  15628  cnopnap  15635  divcncfap  15638  dedekindeulemeu  15646  dedekindicclemeu  15655  ivthinclemlm  15658  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthinclemdisj  15664  ivthdec  15668  ivthreinc  15669  limcimolemlt  15688  limcimo  15689  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  limccoap  15702  eldvap  15706  dvbsssg  15710  dvfgg  15712  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcj  15733  dvfre  15734  dvrecap  15737  plyco  15783  plycj  15785  sin0pilem1  15805  sin0pilem2  15806  pilem3  15807  tanrpcl  15861  tangtx  15862  perfect  16029  lgsne0  16071  lgseisen  16107  lgsquad2lem2  16115  2sqlem8a  16155  2sqlem8  16156  structgrssvtx  16197  edguhgr  16292  umgrpredgv  16302  umgrnloop2  16306  umgr2edg  16362  subuhgr  16427  subumgr  16429  subusgr  16430  wlkpropg  16479  wlkv  16481  wlkvtxeledgg  16499  wlkvtxiedgg  16501  wlk1walkdom  16514  trlsv  16539  clwwlksswrd  16552  clwwlkclwwlkn  16564  eupthv  16601  eupthseg  16607  eupth2lem3lem3fi  16625  eupth2lem3lem4fi  16628  eupth2lemsfi  16633  eulerpathprum  16635  nninfalllem1  16956  iooref1o  16988  alsi1d  17036  alsc1d  17038