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  1021  eldifad  3208  unssad  3381  opth1  4321  opth  4322  0nelop  4333  epelg  4380  poirr  4397  brrelex1  4757  brrelex  4758  asymref  5113  soirri  5122  sotri  5123  ffdmd  5494  fcnvres  5508  fun11iun  5592  funopsn  5816  elmpocl1  6200  f1od  6207  f1o2d  6209  oprssdmm  6315  smoiso  6446  tfrlem1  6452  swoer  6706  ecopovtrn  6777  ecopovtrng  6780  elmapssres  6818  pmresg  6821  mapsspm  6827  en1uniel  6954  pw2f1odc  6992  xpf1o  7001  sbthlemi9  7128  supelti  7165  supsnti  7168  supisoti  7173  ctssdccl  7274  ctfoex  7281  fodjum  7309  en2eleq  7369  djuen  7389  pw1if  7406  dftap2  7433  2omotaplemst  7440  exmidapne  7442  ccfunen  7446  dfplpq2  7537  ltbtwnnqq  7598  enq0tr  7617  elnp1st2nd  7659  prcdnql  7667  prnminu  7672  prloc  7674  genpcdl  7702  addnqprulem  7711  addlocprlemlt  7714  addlocprlemgt  7717  addlocprlem  7718  addlocpr  7719  nqprxx  7729  ltnqex  7732  addnqprlemfl  7742  addnqprlemfu  7743  appdivnq  7746  prmuloclemcalc  7748  prmuloc  7749  mullocprlem  7753  mulnqprlemfl  7758  mulnqprlemfu  7759  ltprordil  7772  ltnqpri  7777  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  ltexpri  7796  lteupri  7800  ltaprlem  7801  recexprlemell  7805  recexprlemelu  7806  recexprlemloc  7814  recexprlempr  7815  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1u  7819  aptipr  7824  cauappcvgprlemm  7828  cauappcvgprlemlol  7830  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlem1  7842  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemlol  7853  caucvgprlemladdfu  7860  caucvgprprlemloccalc  7867  caucvgprprlemnkltj  7872  caucvgprprlemnbj  7876  caucvgprprlemml  7877  caucvgprprlemlol  7881  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  suplocexprlemss  7898  suplocexprlemru  7902  suplocexprlemlub  7907  ltsrprg  7930  caucvgsrlemasr  7973  suplocsrlemb  7989  suplocsrlem  7991  suplocsr  7992  axcaucvglemcau  8081  axpre-suploclemres  8084  negf1o  8524  apreap  8730  apreim  8746  msqge0  8759  mulge0  8762  apti  8765  apsscn  8790  mulap0bad  8802  divadddivap  8870  recnz  9536  lbzbi  9807  xadd4d  10077  ixxss1  10096  ixxss2  10097  ixxss12  10098  iccss2  10136  iccssioo2  10138  iccssico2  10139  iccen  10198  elfzole1  10348  ioom  10475  elicore  10481  flqle  10493  flqltnz  10502  addmodlteq  10615  expclzap  10781  hashennnuni  10996  zfz1isolem1  11057  hashdmprop2dom  11061  swrdsbslen  11193  ccatswrd  11197  ccatpfx  11228  recl  11359  cvg1nlemcau  11490  cvg1nlemres  11491  resqrtth  11537  fimaxre2  11733  climcl  11788  reccn2ap  11819  nnf1o  11882  summodclem3  11886  sumpr  11919  fsump1i  11939  fisumcom2  11944  fsum00  11968  fsumparts  11976  mertenslemi1  12041  prodmodclem3  12081  fprodcom2fi  12132  addsin  12248  subsin  12249  addcos  12252  subcos  12253  sinbnd2  12260  cosbnd2  12261  sin01gt0  12268  cos01gt0  12269  divgcdz  12487  divgcdnn  12491  gcdaddm  12500  bezoutlemstep  12513  dvdsgcdb  12529  dfgcd2  12530  mulgcd  12532  gcdzeq  12538  dvdsmulgcd  12541  sqgcd  12545  bezoutr  12548  lcmval  12580  lcmcllem  12584  gcddvdslcm  12590  lcmgcdlem  12594  lcmgcd  12595  lcmgcdeq  12600  lcmdvdsb  12601  mulgcddvds  12611  rpmulgcd2  12612  qredeu  12614  rpdvds  12616  isprm3  12635  divgcdodd  12660  coprm  12661  rpexp  12670  sqrt2irr  12679  qnumcl  12705  qnumdencoprm  12710  divnumden  12713  numsq  12720  phimullem  12742  eulerthlem1  12744  prmdiveq  12753  prmdivdiv  12754  hashgcdlem  12755  odzcl  12761  reumodprminv  12771  pythagtriplem19  12800  pclemub  12805  pcprendvds  12808  pcprendvds2  12809  pcpre1  12810  pcpremul  12811  pceulem  12812  pceu  12813  pczpre  12815  pczcl  12816  pcgcd1  12846  pc2dvds  12848  pcaddlem  12857  pcmpt  12861  pockthlem  12874  prmunb  12880  4sqlem7  12902  4sqlem8  12903  4sqlem9  12904  4sqlem10  12905  4sqlem14  12922  4sqlem15  12923  4sqlem16  12924  4sqlem17  12925  4sqlem18  12926  ennnfonelemg  12969  ennnfonelemf1  12984  ctiunctlemu1st  13000  nninfdclemf  13015  nninfdclemp1  13016  mgmidcl  13406  gsumfzval  13419  gsumval2  13425  mndlid  13463  prdsmndd  13476  imasmndf1  13482  dfgrp3mlem  13626  grplactf1o  13631  prdsgrpd  13637  prdsinvgd  13638  imasgrpf1  13644  subgsubm  13728  qusgrp  13764  ghmgrp1  13777  ghmf  13779  ghmnsgpreima  13801  kerf1ghm  13806  conjsubg  13809  imasrng  13914  srgdilem  13927  srgdi  13932  srglidm  13937  ringdilem  13970  ringdi  13976  ringlidm  13981  imasring  14022  imasringf1  14023  dvdsrcld  14055  unitcld  14066  unitmulcl  14071  unitnegcl  14088  rhmghm  14120  elrhmunit  14135  subrgss  14180  subrgrcl  14184  lmodvscl  14263  lmodvsdi  14269  lmodvsdir  14270  lsslsp  14387  qusring  14485  crngridl  14488  znunit  14617  znrrg  14618  psrbaglesuppg  14630  psrelbas  14633  psraddcl  14638  mplrcl  14652  uniopn  14669  restbasg  14836  cntop1  14869  cnf  14872  cnpf2  14875  lmtopcnp  14918  psmetdmdm  14992  psmetf  14993  psmet0  14995  xmetf  15018  metf  15019  blhalf  15076  xmetxpbl  15176  ioo2bl  15219  tgioo  15222  cncff  15245  rescncf  15249  cdivcncfap  15272  cnopnap  15279  divcncfap  15282  dedekindeulemeu  15290  dedekindicclemeu  15299  ivthinclemlm  15302  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthinclemdisj  15308  ivthdec  15312  ivthreinc  15313  limcimolemlt  15332  limcimo  15333  limccnpcntop  15343  limccnp2lem  15344  limccnp2cntop  15345  limccoap  15346  eldvap  15350  dvbsssg  15354  dvfgg  15356  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcj  15377  dvfre  15378  dvrecap  15381  plyco  15427  plycj  15429  sin0pilem1  15449  sin0pilem2  15450  pilem3  15451  tanrpcl  15505  tangtx  15506  perfect  15669  lgsne0  15711  lgseisen  15747  lgsquad2lem2  15755  2sqlem8a  15795  2sqlem8  15796  structgrssvtx  15837  edguhgr  15929  umgrpredgv  15939  umgrnloop2  15943  umgr2edg  15999  wlkpropg  16030  wlkvtxeledgg  16041  wlkvtxiedgg  16042  nninfalllem1  16333  iooref1o  16361  alsi1d  16408  alsc1d  16410