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  1000  eldifad  3185  unssad  3358  opth1  4298  opth  4299  0nelop  4310  epelg  4355  poirr  4372  brrelex1  4732  brrelex  4733  asymref  5087  soirri  5096  sotri  5097  ffdmd  5467  fcnvres  5481  fun11iun  5565  funopsn  5785  elmpocl1  6165  f1od  6172  f1o2d  6174  oprssdmm  6280  smoiso  6411  tfrlem1  6417  swoer  6671  ecopovtrn  6742  ecopovtrng  6745  elmapssres  6783  pmresg  6786  mapsspm  6792  en1uniel  6919  pw2f1odc  6957  xpf1o  6966  sbthlemi9  7093  supelti  7130  supsnti  7133  supisoti  7138  ctssdccl  7239  ctfoex  7246  fodjum  7274  en2eleq  7334  djuen  7354  pw1if  7371  dftap2  7398  2omotaplemst  7405  exmidapne  7407  ccfunen  7411  dfplpq2  7502  ltbtwnnqq  7563  enq0tr  7582  elnp1st2nd  7624  prcdnql  7632  prnminu  7637  prloc  7639  genpcdl  7667  addnqprulem  7676  addlocprlemlt  7679  addlocprlemgt  7682  addlocprlem  7683  addlocpr  7684  nqprxx  7694  ltnqex  7697  addnqprlemfl  7707  addnqprlemfu  7708  appdivnq  7711  prmuloclemcalc  7713  prmuloc  7714  mullocprlem  7718  mulnqprlemfl  7723  mulnqprlemfu  7724  ltprordil  7737  ltnqpri  7742  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemlol  7750  ltexprlemopu  7751  ltexprlemupu  7752  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemfl  7757  ltexprlemrl  7758  ltexprlemfu  7759  ltexprlemru  7760  ltexpri  7761  lteupri  7765  ltaprlem  7766  recexprlemell  7770  recexprlemelu  7771  recexprlemloc  7779  recexprlempr  7780  recexprlem1ssl  7781  recexprlem1ssu  7782  recexprlemss1u  7784  aptipr  7789  cauappcvgprlemm  7793  cauappcvgprlemlol  7795  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlem1  7807  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemlol  7818  caucvgprlemladdfu  7825  caucvgprprlemloccalc  7832  caucvgprprlemnkltj  7837  caucvgprprlemnbj  7841  caucvgprprlemml  7842  caucvgprprlemlol  7846  caucvgprprlemloc  7851  caucvgprprlemexbt  7854  suplocexprlemss  7863  suplocexprlemru  7867  suplocexprlemlub  7872  ltsrprg  7895  caucvgsrlemasr  7938  suplocsrlemb  7954  suplocsrlem  7956  suplocsr  7957  axcaucvglemcau  8046  axpre-suploclemres  8049  negf1o  8489  apreap  8695  apreim  8711  msqge0  8724  mulge0  8727  apti  8730  apsscn  8755  mulap0bad  8767  divadddivap  8835  recnz  9501  lbzbi  9772  xadd4d  10042  ixxss1  10061  ixxss2  10062  ixxss12  10063  iccss2  10101  iccssioo2  10103  iccssico2  10104  iccen  10163  elfzole1  10313  ioom  10440  elicore  10446  flqle  10458  flqltnz  10467  addmodlteq  10580  expclzap  10746  hashennnuni  10961  zfz1isolem1  11022  hashdmprop2dom  11026  swrdsbslen  11157  ccatswrd  11161  ccatpfx  11192  recl  11279  cvg1nlemcau  11410  cvg1nlemres  11411  resqrtth  11457  fimaxre2  11653  climcl  11708  reccn2ap  11739  nnf1o  11802  summodclem3  11806  sumpr  11839  fsump1i  11859  fisumcom2  11864  fsum00  11888  fsumparts  11896  mertenslemi1  11961  prodmodclem3  12001  fprodcom2fi  12052  addsin  12168  subsin  12169  addcos  12172  subcos  12173  sinbnd2  12180  cosbnd2  12181  sin01gt0  12188  cos01gt0  12189  divgcdz  12407  divgcdnn  12411  gcdaddm  12420  bezoutlemstep  12433  dvdsgcdb  12449  dfgcd2  12450  mulgcd  12452  gcdzeq  12458  dvdsmulgcd  12461  sqgcd  12465  bezoutr  12468  lcmval  12500  lcmcllem  12504  gcddvdslcm  12510  lcmgcdlem  12514  lcmgcd  12515  lcmgcdeq  12520  lcmdvdsb  12521  mulgcddvds  12531  rpmulgcd2  12532  qredeu  12534  rpdvds  12536  isprm3  12555  divgcdodd  12580  coprm  12581  rpexp  12590  sqrt2irr  12599  qnumcl  12625  qnumdencoprm  12630  divnumden  12633  numsq  12640  phimullem  12662  eulerthlem1  12664  prmdiveq  12673  prmdivdiv  12674  hashgcdlem  12675  odzcl  12681  reumodprminv  12691  pythagtriplem19  12720  pclemub  12725  pcprendvds  12728  pcprendvds2  12729  pcpre1  12730  pcpremul  12731  pceulem  12732  pceu  12733  pczpre  12735  pczcl  12736  pcgcd1  12766  pc2dvds  12768  pcaddlem  12777  pcmpt  12781  pockthlem  12794  prmunb  12800  4sqlem7  12822  4sqlem8  12823  4sqlem9  12824  4sqlem10  12825  4sqlem14  12842  4sqlem15  12843  4sqlem16  12844  4sqlem17  12845  4sqlem18  12846  ennnfonelemg  12889  ennnfonelemf1  12904  ctiunctlemu1st  12920  nninfdclemf  12935  nninfdclemp1  12936  mgmidcl  13325  gsumfzval  13338  gsumval2  13344  mndlid  13382  prdsmndd  13395  imasmndf1  13401  dfgrp3mlem  13545  grplactf1o  13550  prdsgrpd  13556  prdsinvgd  13557  imasgrpf1  13563  subgsubm  13647  qusgrp  13683  ghmgrp1  13696  ghmf  13698  ghmnsgpreima  13720  kerf1ghm  13725  conjsubg  13728  imasrng  13833  srgdilem  13846  srgdi  13851  srglidm  13856  ringdilem  13889  ringdi  13895  ringlidm  13900  imasring  13941  imasringf1  13942  dvdsrcld  13974  unitcld  13985  unitmulcl  13990  unitnegcl  14007  rhmghm  14039  elrhmunit  14054  subrgss  14099  subrgrcl  14103  lmodvscl  14182  lmodvsdi  14188  lmodvsdir  14189  lsslsp  14306  qusring  14404  crngridl  14407  znunit  14536  znrrg  14537  psrbaglesuppg  14549  psrelbas  14552  psraddcl  14557  mplrcl  14571  uniopn  14588  restbasg  14755  cntop1  14788  cnf  14791  cnpf2  14794  lmtopcnp  14837  psmetdmdm  14911  psmetf  14912  psmet0  14914  xmetf  14937  metf  14938  blhalf  14995  xmetxpbl  15095  ioo2bl  15138  tgioo  15141  cncff  15164  rescncf  15168  cdivcncfap  15191  cnopnap  15198  divcncfap  15201  dedekindeulemeu  15209  dedekindicclemeu  15218  ivthinclemlm  15221  ivthinclemlopn  15223  ivthinclemuopn  15225  ivthinclemdisj  15227  ivthdec  15231  ivthreinc  15232  limcimolemlt  15251  limcimo  15252  limccnpcntop  15262  limccnp2lem  15263  limccnp2cntop  15264  limccoap  15265  eldvap  15269  dvbsssg  15273  dvfgg  15275  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvcj  15296  dvfre  15297  dvrecap  15300  plyco  15346  plycj  15348  sin0pilem1  15368  sin0pilem2  15369  pilem3  15370  tanrpcl  15424  tangtx  15425  perfect  15588  lgsne0  15630  lgseisen  15666  lgsquad2lem2  15674  2sqlem8a  15714  2sqlem8  15715  structgrssvtx  15756  edguhgr  15843  umgrpredgv  15851  umgrnloop2  15855  nninfalllem1  16147  iooref1o  16175  alsi1d  16222  alsc1d  16224