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  7342  supsnti  7345  supisoti  7350  ctssdccl  7451  ctfoex  7458  fodjum  7486  en2eleq  7547  djuen  7567  pw1if  7584  dftap2  7617  2omotaplemst  7624  exmidapne  7626  ccfunen  7630  dfplpq2  7721  ltbtwnnqq  7782  enq0tr  7801  elnp1st2nd  7843  prcdnql  7851  prnminu  7856  prloc  7858  genpcdl  7886  addnqprulem  7895  addlocprlemlt  7898  addlocprlemgt  7901  addlocprlem  7902  addlocpr  7903  nqprxx  7913  ltnqex  7916  addnqprlemfl  7926  addnqprlemfu  7927  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mullocprlem  7937  mulnqprlemfl  7942  mulnqprlemfu  7943  ltprordil  7956  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltexpri  7980  lteupri  7984  ltaprlem  7985  recexprlemell  7989  recexprlemelu  7990  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1u  8003  aptipr  8008  cauappcvgprlemm  8012  cauappcvgprlemlol  8014  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlem1  8026  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemlol  8037  caucvgprlemladdfu  8044  caucvgprprlemloccalc  8051  caucvgprprlemnkltj  8056  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemlol  8065  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  suplocexprlemss  8082  suplocexprlemru  8086  suplocexprlemlub  8091  ltsrprg  8114  caucvgsrlemasr  8157  suplocsrlemb  8173  suplocsrlem  8175  suplocsr  8176  axcaucvglemcau  8265  axpre-suploclemres  8268  negf1o  8710  apreap  8917  apreim  8933  msqge0  8946  mulge0  8949  apti  8952  apsscn  8977  mulap0bad  8989  divadddivap  9059  recnz  9743  lbzbi  10025  xadd4d  10297  ixxss1  10316  ixxss2  10317  ixxss12  10318  iccss2  10356  iccssioo2  10358  iccssico2  10359  iccen  10419  elfzole1  10573  infssfzcldc  10679  infssfzledc  10680  ioom  10705  elicore  10711  flqle  10725  flapge  10730  flqltnz  10735  addmodlteq  10848  expclzap  11014  hashennnuni  11232  zfz1isolem1  11306  hashdmprop2dom  11310  swrdsbslen  11452  ccatswrd  11456  ccatpfx  11487  recl  11632  sq01  11674  cvg1nlemcau  11764  cvg1nlemres  11765  resqrtth  11811  fimaxre2  12008  climcl  12064  reccn2ap  12095  nnf1o  12159  summodclem3  12163  sumpr  12196  fsump1i  12216  fisumcom2  12221  fsum00  12245  fsumparts  12253  mertenslemi1  12318  prodmodclem3  12358  fprodcom2fi  12409  addsin  12525  subsin  12526  addcos  12529  subcos  12530  sinbnd2  12537  cosbnd2  12538  sin01gt0  12545  cos01gt0  12546  divgcdz  12764  divgcdnn  12768  gcdaddm  12777  bezoutlemstep  12790  dvdsgcdb  12806  dfgcd2  12807  mulgcd  12809  gcdzeq  12815  dvdsmulgcd  12818  sqgcd  12822  bezoutr  12825  lcmval  12857  lcmcllem  12861  gcddvdslcm  12867  lcmgcdlem  12871  lcmgcd  12872  lcmgcdeq  12877  lcmdvdsb  12878  mulgcddvds  12888  rpmulgcd2  12889  qredeu  12891  rpdvds  12893  isprm3  12912  divgcdodd  12938  coprm  12939  rpexp  12948  sqrt2irr  12957  qnumcl  12984  qnumdencoprm  12989  divnumden  12992  numsq  12999  phimullem  13023  eulerthlem1  13025  prmdiveq  13034  prmdivdiv  13035  hashgcdlem  13036  odzcl  13042  reumodprminv  13052  pythagtriplem19  13081  pclemub  13086  pcprendvds  13089  pcprendvds2  13090  pcpre1  13091  pcpremul  13092  pceulem  13093  pceu  13094  pczpre  13096  pczcl  13097  pcgcd1  13127  pc2dvds  13129  pcaddlem  13138  pcmpt  13142  pockthlem  13155  prmunb  13161  4sqlem7  13183  4sqlem8  13184  4sqlem9  13185  4sqlem10  13186  4sqlem14  13203  4sqlem15  13204  4sqlem16  13205  4sqlem17  13206  4sqlem18  13207  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemimin  13298  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsv  13302  ballotfilemsgt1  13303  ballotfilemsdom  13304  ballotfilemsel1i  13305  ballotfilemsf1o  13306  ballotfilemsi  13307  ballotfilemsima  13308  ballotfilemscr  13311  ballotfilemrv  13312  ballotfilemrv2  13314  ballotfilemro  13315  ballotfilemfrc  13319  ballotfilemfrci  13320  ballotfilemfrceq  13321  ballotfilemfrcn0  13322  ballotfilemrc  13323  ballotfilemirc  13324  ballotfilemrinv0  13325  ballotfilem1ri  13327  ennnfonelemg  13343  ennnfonelemf1  13358  ctiunctlemu1st  13374  nninfdclemf  13389  nninfdclemp1  13390  mgmidcl  13747  gzsumfzval  13760  gzsumval2  13763  mndlid  13797  imasmndf1  13810  dfgrp3mlem  13952  grplactf1o  13957  imasgrpf1  13964  subgsubm  14048  qusgrp  14084  ghmgrp1  14097  ghmf  14099  ghmnsgpreima  14121  kerf1ghm  14126  conjsubg  14129  gzsumsplit0  14197  gsumvalfi  14201  prdsmndd  14243  prdsgrpd  14246  prdsinvgd  14247  imasrng  14304  srgdilem  14322  srgdi  14327  srglidm  14332  ringdilem  14365  ringdi  14372  ringlidm  14377  imasring  14418  imasringf1  14419  dvdsrcld  14453  unitcld  14464  unitmulcl  14469  unitnegcl  14486  rhmghm  14518  elrhmunit  14533  subrgss  14579  subrgrcl  14583  rrgsupp  14623  lmodvscl  14690  lmodvsdi  14697  lmodvsdir  14698  lsslsp  14815  qusring  14913  crngridl  14916  znunit  15043  znrrg  15044  assaass  15053  assalmod  15055  psrbaglesuppg  15106  psrbagcon  15111  psrbagconcl  15112  psrelbas  15115  psraddcl  15120  mplrcl  15134  uniopn  15151  restbasg  15318  cntop1  15351  cnf  15354  cnpf2  15357  lmtopcnp  15400  psmetdmdm  15474  psmetf  15475  psmet0  15477  xmetf  15500  metf  15501  blhalf  15558  xmetxpbl  15658  ioo2bl  15701  tgioo  15704  cncff  15727  rescncf  15731  cdivcncfap  15754  cnopnap  15761  divcncfap  15764  dedekindeulemeu  15772  dedekindicclemeu  15781  ivthinclemlm  15784  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthinclemdisj  15790  ivthdec  15794  ivthreinc  15795  limcimolemlt  15814  limcimo  15815  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  limccoap  15828  eldvap  15832  dvbsssg  15836  dvfgg  15838  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcj  15859  dvfre  15860  dvrecap  15863  plyco  15909  plycj  15911  sin0pilem1  15932  sin0pilem2  15933  pilem3  15934  tanrpcl  15988  tangtx  15989  zprmlogbaplem2  16135  zprmlogbaplem3  16136  ppiqsval2  16157  perfect  16199  bposlem1  16209  bposlem4  16212  bposlem5  16213  lgsne0  16255  lgseisen  16291  lgsquad2lem2  16299  2sqlem8a  16339  2sqlem8  16340  structgrssvtx  16381  edguhgr  16476  umgrpredgv  16486  umgrnloop2  16490  umgr2edg  16546  subuhgr  16611  subumgr  16613  subusgr  16614  wlkpropg  16663  wlkv  16665  wlkvtxeledgg  16683  wlkvtxiedgg  16685  wlk1walkdom  16698  trlsv  16723  clwwlksswrd  16736  clwwlkclwwlkn  16748  eupthv  16785  eupthseg  16791  eupth2lem3lem3fi  16809  eupth2lem3lem4fi  16812  eupth2lemsfi  16817  eulerpathprum  16819  nninfalllem1  17149  iooref1o  17181  als1d  17231  rals1d  17233  alseu1d  17267  ralseu1d  17269