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  3225  unssad  3400  opth1  4357  opth  4358  0nelop  4369  epelg  4416  poirr  4433  brrelex1  4794  brrelex  4795  asymref  5153  soirri  5162  sotri  5163  ffdmd  5539  fcnvres  5555  fun11iun  5640  funopsn  5865  elmpocl1  6258  f1od  6266  f1o2d  6268  oprssdmm  6378  elmpom  6447  fczsupp0  6472  smoiso  6546  tfrlem1  6552  swoer  6808  ecopovtrn  6879  ecopovtrng  6882  elmapssres  6920  pmresg  6923  mapsspm  6929  en1uniel  7057  pw2f1odc  7101  xpf1o  7110  sbthlemi9  7248  fsuppfund  7260  supelti  7306  supsnti  7309  supisoti  7314  ctssdccl  7415  ctfoex  7422  fodjum  7450  en2eleq  7511  djuen  7531  pw1if  7548  dftap2  7581  2omotaplemst  7588  exmidapne  7590  ccfunen  7594  dfplpq2  7685  ltbtwnnqq  7746  enq0tr  7765  elnp1st2nd  7807  prcdnql  7815  prnminu  7820  prloc  7822  genpcdl  7850  addnqprulem  7859  addlocprlemlt  7862  addlocprlemgt  7865  addlocprlem  7866  addlocpr  7867  nqprxx  7877  ltnqex  7880  addnqprlemfl  7890  addnqprlemfu  7891  appdivnq  7894  prmuloclemcalc  7896  prmuloc  7897  mullocprlem  7901  mulnqprlemfl  7906  mulnqprlemfu  7907  ltprordil  7920  ltnqpri  7925  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  ltexpri  7944  lteupri  7948  ltaprlem  7949  recexprlemell  7953  recexprlemelu  7954  recexprlemloc  7962  recexprlempr  7963  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1u  7967  aptipr  7972  cauappcvgprlemm  7976  cauappcvgprlemlol  7978  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlem1  7990  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemlol  8001  caucvgprlemladdfu  8008  caucvgprprlemloccalc  8015  caucvgprprlemnkltj  8020  caucvgprprlemnbj  8024  caucvgprprlemml  8025  caucvgprprlemlol  8029  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  suplocexprlemss  8046  suplocexprlemru  8050  suplocexprlemlub  8055  ltsrprg  8078  caucvgsrlemasr  8121  suplocsrlemb  8137  suplocsrlem  8139  suplocsr  8140  axcaucvglemcau  8229  axpre-suploclemres  8232  negf1o  8672  apreap  8878  apreim  8894  msqge0  8907  mulge0  8910  apti  8913  apsscn  8938  mulap0bad  8950  divadddivap  9018  recnz  9689  lbzbi  9966  xadd4d  10237  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccss2  10296  iccssioo2  10298  iccssico2  10299  iccen  10359  elfzole1  10512  infssfzcldc  10618  infssfzledc  10619  ioom  10644  elicore  10650  flqle  10662  flqltnz  10671  addmodlteq  10784  expclzap  10950  hashennnuni  11167  zfz1isolem1  11237  hashdmprop2dom  11241  swrdsbslen  11383  ccatswrd  11387  ccatpfx  11418  recl  11563  cvg1nlemcau  11694  cvg1nlemres  11695  resqrtth  11741  fimaxre2  11937  climcl  11992  reccn2ap  12023  nnf1o  12087  summodclem3  12091  sumpr  12124  fsump1i  12144  fisumcom2  12149  fsum00  12173  fsumparts  12181  mertenslemi1  12246  prodmodclem3  12286  fprodcom2fi  12337  addsin  12453  subsin  12454  addcos  12457  subcos  12458  sinbnd2  12465  cosbnd2  12466  sin01gt0  12473  cos01gt0  12474  divgcdz  12692  divgcdnn  12696  gcdaddm  12705  bezoutlemstep  12718  dvdsgcdb  12734  dfgcd2  12735  mulgcd  12737  gcdzeq  12743  dvdsmulgcd  12746  sqgcd  12750  bezoutr  12753  lcmval  12785  lcmcllem  12789  gcddvdslcm  12795  lcmgcdlem  12799  lcmgcd  12800  lcmgcdeq  12805  lcmdvdsb  12806  mulgcddvds  12816  rpmulgcd2  12817  qredeu  12819  rpdvds  12821  isprm3  12840  divgcdodd  12865  coprm  12866  rpexp  12875  sqrt2irr  12884  qnumcl  12910  qnumdencoprm  12915  divnumden  12918  numsq  12925  phimullem  12947  eulerthlem1  12949  prmdiveq  12958  prmdivdiv  12959  hashgcdlem  12960  odzcl  12966  reumodprminv  12976  pythagtriplem19  13005  pclemub  13010  pcprendvds  13013  pcprendvds2  13014  pcpre1  13015  pcpremul  13016  pceulem  13017  pceu  13018  pczpre  13020  pczcl  13021  pcgcd1  13051  pc2dvds  13053  pcaddlem  13062  pcmpt  13066  pockthlem  13079  prmunb  13085  4sqlem7  13107  4sqlem8  13108  4sqlem9  13109  4sqlem10  13110  4sqlem14  13127  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  4sqlem18  13131  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemimin  13193  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsv  13197  ballotfilemsgt1  13198  ballotfilemsdom  13199  ballotfilemsel1i  13200  ballotfilemsf1o  13201  ballotfilemsi  13202  ballotfilemsima  13203  ballotfilemscr  13206  ballotfilemrv  13207  ballotfilemrv2  13209  ballotfilemro  13210  ballotfilemfrc  13214  ballotfilemfrci  13215  ballotfilemfrceq  13216  ballotfilemfrcn0  13217  ballotfilemrc  13218  ballotfilemirc  13219  ballotfilemrinv0  13220  ballotfilem1ri  13222  ennnfonelemg  13238  ennnfonelemf1  13253  ctiunctlemu1st  13269  nninfdclemf  13284  nninfdclemp1  13285  mgmidcl  13641  gsumfzval  13654  gsumval2  13660  mndlid  13696  imasmndf1  13709  dfgrp3mlem  13853  grplactf1o  13858  imasgrpf1  13865  subgsubm  13949  qusgrp  13985  ghmgrp1  13998  ghmf  14000  ghmnsgpreima  14022  kerf1ghm  14027  conjsubg  14030  gsumsplit0  14099  gfsumval  14102  prdsmndd  14136  prdsgrpd  14139  prdsinvgd  14140  imasrng  14195  srgdilem  14212  srgdi  14217  srglidm  14222  ringdilem  14255  ringdi  14261  ringlidm  14266  imasring  14307  imasringf1  14308  dvdsrcld  14342  unitcld  14353  unitmulcl  14358  unitnegcl  14375  rhmghm  14407  elrhmunit  14422  subrgss  14468  subrgrcl  14472  rrgsupp  14512  lmodvscl  14579  lmodvsdi  14585  lmodvsdir  14586  lsslsp  14703  qusring  14801  crngridl  14804  znunit  14933  znrrg  14934  psrbaglesuppg  14947  psrbagcon  14952  psrbagconcl  14953  psrelbas  14956  psraddcl  14961  mplrcl  14975  uniopn  14992  restbasg  15159  cntop1  15192  cnf  15195  cnpf2  15198  lmtopcnp  15241  psmetdmdm  15315  psmetf  15316  psmet0  15318  xmetf  15341  metf  15342  blhalf  15399  xmetxpbl  15499  ioo2bl  15542  tgioo  15545  cncff  15568  rescncf  15572  cdivcncfap  15595  cnopnap  15602  divcncfap  15605  dedekindeulemeu  15613  dedekindicclemeu  15622  ivthinclemlm  15625  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthinclemdisj  15631  ivthdec  15635  ivthreinc  15636  limcimolemlt  15655  limcimo  15656  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  limccoap  15669  eldvap  15673  dvbsssg  15677  dvfgg  15679  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcj  15700  dvfre  15701  dvrecap  15704  plyco  15750  plycj  15752  sin0pilem1  15772  sin0pilem2  15773  pilem3  15774  tanrpcl  15828  tangtx  15829  perfect  15995  lgsne0  16037  lgseisen  16073  lgsquad2lem2  16081  2sqlem8a  16121  2sqlem8  16122  structgrssvtx  16163  edguhgr  16258  umgrpredgv  16268  umgrnloop2  16272  umgr2edg  16328  subuhgr  16393  subumgr  16395  subusgr  16396  wlkpropg  16445  wlkv  16447  wlkvtxeledgg  16465  wlkvtxiedgg  16467  wlk1walkdom  16480  trlsv  16505  clwwlksswrd  16518  clwwlkclwwlkn  16530  eupthv  16567  eupthseg  16573  eupth2lem3lem3fi  16591  eupth2lem3lem4fi  16594  eupth2lemsfi  16599  eulerpathprum  16601  nninfalllem1  16912  iooref1o  16944  alsi1d  16993  alsc1d  16995