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  1023  eldifad  3211  unssad  3384  opth1  4328  opth  4329  0nelop  4340  epelg  4387  poirr  4404  brrelex1  4765  brrelex  4766  asymref  5122  soirri  5131  sotri  5132  ffdmd  5506  fcnvres  5520  fun11iun  5604  funopsn  5830  elmpocl1  6218  f1od  6226  f1o2d  6228  oprssdmm  6334  elmpom  6403  smoiso  6468  tfrlem1  6474  swoer  6730  ecopovtrn  6801  ecopovtrng  6804  elmapssres  6842  pmresg  6845  mapsspm  6851  en1uniel  6978  pw2f1odc  7021  xpf1o  7030  sbthlemi9  7164  supelti  7201  supsnti  7204  supisoti  7209  ctssdccl  7310  ctfoex  7317  fodjum  7345  en2eleq  7406  djuen  7426  pw1if  7443  dftap2  7470  2omotaplemst  7477  exmidapne  7479  ccfunen  7483  dfplpq2  7574  ltbtwnnqq  7635  enq0tr  7654  elnp1st2nd  7696  prcdnql  7704  prnminu  7709  prloc  7711  genpcdl  7739  addnqprulem  7748  addlocprlemlt  7751  addlocprlemgt  7754  addlocprlem  7755  addlocpr  7756  nqprxx  7766  ltnqex  7769  addnqprlemfl  7779  addnqprlemfu  7780  appdivnq  7783  prmuloclemcalc  7785  prmuloc  7786  mullocprlem  7790  mulnqprlemfl  7795  mulnqprlemfu  7796  ltprordil  7809  ltnqpri  7814  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  ltexpri  7833  lteupri  7837  ltaprlem  7838  recexprlemell  7842  recexprlemelu  7843  recexprlemloc  7851  recexprlempr  7852  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1u  7856  aptipr  7861  cauappcvgprlemm  7865  cauappcvgprlemlol  7867  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemlol  7890  caucvgprlemladdfu  7897  caucvgprprlemloccalc  7904  caucvgprprlemnkltj  7909  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemlol  7918  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  suplocexprlemss  7935  suplocexprlemru  7939  suplocexprlemlub  7944  ltsrprg  7967  caucvgsrlemasr  8010  suplocsrlemb  8026  suplocsrlem  8028  suplocsr  8029  axcaucvglemcau  8118  axpre-suploclemres  8121  negf1o  8561  apreap  8767  apreim  8783  msqge0  8796  mulge0  8799  apti  8802  apsscn  8827  mulap0bad  8839  divadddivap  8907  recnz  9573  lbzbi  9850  xadd4d  10120  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iccssioo2  10181  iccssico2  10182  iccen  10241  elfzole1  10391  ioom  10521  elicore  10527  flqle  10539  flqltnz  10548  addmodlteq  10661  expclzap  10827  hashennnuni  11042  zfz1isolem1  11105  hashdmprop2dom  11109  swrdsbslen  11248  ccatswrd  11252  ccatpfx  11283  recl  11415  cvg1nlemcau  11546  cvg1nlemres  11547  resqrtth  11593  fimaxre2  11789  climcl  11844  reccn2ap  11875  nnf1o  11939  summodclem3  11943  sumpr  11976  fsump1i  11996  fisumcom2  12001  fsum00  12025  fsumparts  12033  mertenslemi1  12098  prodmodclem3  12138  fprodcom2fi  12189  addsin  12305  subsin  12306  addcos  12309  subcos  12310  sinbnd2  12317  cosbnd2  12318  sin01gt0  12325  cos01gt0  12326  divgcdz  12544  divgcdnn  12548  gcdaddm  12557  bezoutlemstep  12570  dvdsgcdb  12586  dfgcd2  12587  mulgcd  12589  gcdzeq  12595  dvdsmulgcd  12598  sqgcd  12602  bezoutr  12605  lcmval  12637  lcmcllem  12641  gcddvdslcm  12647  lcmgcdlem  12651  lcmgcd  12652  lcmgcdeq  12657  lcmdvdsb  12658  mulgcddvds  12668  rpmulgcd2  12669  qredeu  12671  rpdvds  12673  isprm3  12692  divgcdodd  12717  coprm  12718  rpexp  12727  sqrt2irr  12736  qnumcl  12762  qnumdencoprm  12767  divnumden  12770  numsq  12777  phimullem  12799  eulerthlem1  12801  prmdiveq  12810  prmdivdiv  12811  hashgcdlem  12812  odzcl  12818  reumodprminv  12828  pythagtriplem19  12857  pclemub  12862  pcprendvds  12865  pcprendvds2  12866  pcpre1  12867  pcpremul  12868  pceulem  12869  pceu  12870  pczpre  12872  pczcl  12873  pcgcd1  12903  pc2dvds  12905  pcaddlem  12914  pcmpt  12918  pockthlem  12931  prmunb  12937  4sqlem7  12959  4sqlem8  12960  4sqlem9  12961  4sqlem10  12962  4sqlem14  12979  4sqlem15  12980  4sqlem16  12981  4sqlem17  12982  4sqlem18  12983  ennnfonelemg  13026  ennnfonelemf1  13041  ctiunctlemu1st  13057  nninfdclemf  13072  nninfdclemp1  13073  mgmidcl  13463  gsumfzval  13476  gsumval2  13482  mndlid  13520  prdsmndd  13533  imasmndf1  13539  dfgrp3mlem  13683  grplactf1o  13688  prdsgrpd  13694  prdsinvgd  13695  imasgrpf1  13701  subgsubm  13785  qusgrp  13821  ghmgrp1  13834  ghmf  13836  ghmnsgpreima  13858  kerf1ghm  13863  conjsubg  13866  gsumsplit0  13935  imasrng  13972  srgdilem  13985  srgdi  13990  srglidm  13995  ringdilem  14028  ringdi  14034  ringlidm  14039  imasring  14080  imasringf1  14081  dvdsrcld  14114  unitcld  14125  unitmulcl  14130  unitnegcl  14147  rhmghm  14179  elrhmunit  14194  subrgss  14239  subrgrcl  14243  lmodvscl  14322  lmodvsdi  14328  lmodvsdir  14329  lsslsp  14446  qusring  14544  crngridl  14547  znunit  14676  znrrg  14677  psrbaglesuppg  14689  psrelbas  14692  psraddcl  14697  mplrcl  14711  uniopn  14728  restbasg  14895  cntop1  14928  cnf  14931  cnpf2  14934  lmtopcnp  14977  psmetdmdm  15051  psmetf  15052  psmet0  15054  xmetf  15077  metf  15078  blhalf  15135  xmetxpbl  15235  ioo2bl  15278  tgioo  15281  cncff  15304  rescncf  15308  cdivcncfap  15331  cnopnap  15338  divcncfap  15341  dedekindeulemeu  15349  dedekindicclemeu  15358  ivthinclemlm  15361  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthinclemdisj  15367  ivthdec  15371  ivthreinc  15372  limcimolemlt  15391  limcimo  15392  limccnpcntop  15402  limccnp2lem  15403  limccnp2cntop  15404  limccoap  15405  eldvap  15409  dvbsssg  15413  dvfgg  15415  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvcj  15436  dvfre  15437  dvrecap  15440  plyco  15486  plycj  15488  sin0pilem1  15508  sin0pilem2  15509  pilem3  15510  tanrpcl  15564  tangtx  15565  perfect  15728  lgsne0  15770  lgseisen  15806  lgsquad2lem2  15814  2sqlem8a  15854  2sqlem8  15855  structgrssvtx  15896  edguhgr  15991  umgrpredgv  16001  umgrnloop2  16005  umgr2edg  16061  subuhgr  16126  subumgr  16128  subusgr  16129  wlkpropg  16178  wlkv  16180  wlkvtxeledgg  16198  wlkvtxiedgg  16200  wlk1walkdom  16213  trlsv  16238  clwwlksswrd  16251  clwwlkclwwlkn  16263  eupthv  16300  eupthseg  16306  eupth2lem3lem3fi  16324  eupth2lem3lem4fi  16327  eupth2lemsfi  16332  nninfalllem1  16631  iooref1o  16659  gfsumval  16701  alsi1d  16716  alsc1d  16718