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  5829  elmpocl1  6217  f1od  6225  f1o2d  6227  oprssdmm  6333  elmpom  6402  smoiso  6467  tfrlem1  6473  swoer  6729  ecopovtrn  6800  ecopovtrng  6803  elmapssres  6841  pmresg  6844  mapsspm  6850  en1uniel  6977  pw2f1odc  7020  xpf1o  7029  sbthlemi9  7163  supelti  7200  supsnti  7203  supisoti  7208  ctssdccl  7309  ctfoex  7316  fodjum  7344  en2eleq  7405  djuen  7425  pw1if  7442  dftap2  7469  2omotaplemst  7476  exmidapne  7478  ccfunen  7482  dfplpq2  7573  ltbtwnnqq  7634  enq0tr  7653  elnp1st2nd  7695  prcdnql  7703  prnminu  7708  prloc  7710  genpcdl  7738  addnqprulem  7747  addlocprlemlt  7750  addlocprlemgt  7753  addlocprlem  7754  addlocpr  7755  nqprxx  7765  ltnqex  7768  addnqprlemfl  7778  addnqprlemfu  7779  appdivnq  7782  prmuloclemcalc  7784  prmuloc  7785  mullocprlem  7789  mulnqprlemfl  7794  mulnqprlemfu  7795  ltprordil  7808  ltnqpri  7813  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  ltexpri  7832  lteupri  7836  ltaprlem  7837  recexprlemell  7841  recexprlemelu  7842  recexprlemloc  7850  recexprlempr  7851  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1u  7855  aptipr  7860  cauappcvgprlemm  7864  cauappcvgprlemlol  7866  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlem1  7878  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemlol  7889  caucvgprlemladdfu  7896  caucvgprprlemloccalc  7903  caucvgprprlemnkltj  7908  caucvgprprlemnbj  7912  caucvgprprlemml  7913  caucvgprprlemlol  7917  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  suplocexprlemss  7934  suplocexprlemru  7938  suplocexprlemlub  7943  ltsrprg  7966  caucvgsrlemasr  8009  suplocsrlemb  8025  suplocsrlem  8027  suplocsr  8028  axcaucvglemcau  8117  axpre-suploclemres  8120  negf1o  8560  apreap  8766  apreim  8782  msqge0  8795  mulge0  8798  apti  8801  apsscn  8826  mulap0bad  8838  divadddivap  8906  recnz  9572  lbzbi  9849  xadd4d  10119  ixxss1  10138  ixxss2  10139  ixxss12  10140  iccss2  10178  iccssioo2  10180  iccssico2  10181  iccen  10240  elfzole1  10390  ioom  10519  elicore  10525  flqle  10537  flqltnz  10546  addmodlteq  10659  expclzap  10825  hashennnuni  11040  zfz1isolem1  11103  hashdmprop2dom  11107  swrdsbslen  11246  ccatswrd  11250  ccatpfx  11281  recl  11413  cvg1nlemcau  11544  cvg1nlemres  11545  resqrtth  11591  fimaxre2  11787  climcl  11842  reccn2ap  11873  nnf1o  11936  summodclem3  11940  sumpr  11973  fsump1i  11993  fisumcom2  11998  fsum00  12022  fsumparts  12030  mertenslemi1  12095  prodmodclem3  12135  fprodcom2fi  12186  addsin  12302  subsin  12303  addcos  12306  subcos  12307  sinbnd2  12314  cosbnd2  12315  sin01gt0  12322  cos01gt0  12323  divgcdz  12541  divgcdnn  12545  gcdaddm  12554  bezoutlemstep  12567  dvdsgcdb  12583  dfgcd2  12584  mulgcd  12586  gcdzeq  12592  dvdsmulgcd  12595  sqgcd  12599  bezoutr  12602  lcmval  12634  lcmcllem  12638  gcddvdslcm  12644  lcmgcdlem  12648  lcmgcd  12649  lcmgcdeq  12654  lcmdvdsb  12655  mulgcddvds  12665  rpmulgcd2  12666  qredeu  12668  rpdvds  12670  isprm3  12689  divgcdodd  12714  coprm  12715  rpexp  12724  sqrt2irr  12733  qnumcl  12759  qnumdencoprm  12764  divnumden  12767  numsq  12774  phimullem  12796  eulerthlem1  12798  prmdiveq  12807  prmdivdiv  12808  hashgcdlem  12809  odzcl  12815  reumodprminv  12825  pythagtriplem19  12854  pclemub  12859  pcprendvds  12862  pcprendvds2  12863  pcpre1  12864  pcpremul  12865  pceulem  12866  pceu  12867  pczpre  12869  pczcl  12870  pcgcd1  12900  pc2dvds  12902  pcaddlem  12911  pcmpt  12915  pockthlem  12928  prmunb  12934  4sqlem7  12956  4sqlem8  12957  4sqlem9  12958  4sqlem10  12959  4sqlem14  12976  4sqlem15  12977  4sqlem16  12978  4sqlem17  12979  4sqlem18  12980  ennnfonelemg  13023  ennnfonelemf1  13038  ctiunctlemu1st  13054  nninfdclemf  13069  nninfdclemp1  13070  mgmidcl  13460  gsumfzval  13473  gsumval2  13479  mndlid  13517  prdsmndd  13530  imasmndf1  13536  dfgrp3mlem  13680  grplactf1o  13685  prdsgrpd  13691  prdsinvgd  13692  imasgrpf1  13698  subgsubm  13782  qusgrp  13818  ghmgrp1  13831  ghmf  13833  ghmnsgpreima  13855  kerf1ghm  13860  conjsubg  13863  imasrng  13968  srgdilem  13981  srgdi  13986  srglidm  13991  ringdilem  14024  ringdi  14030  ringlidm  14035  imasring  14076  imasringf1  14077  dvdsrcld  14110  unitcld  14121  unitmulcl  14126  unitnegcl  14143  rhmghm  14175  elrhmunit  14190  subrgss  14235  subrgrcl  14239  lmodvscl  14318  lmodvsdi  14324  lmodvsdir  14325  lsslsp  14442  qusring  14540  crngridl  14543  znunit  14672  znrrg  14673  psrbaglesuppg  14685  psrelbas  14688  psraddcl  14693  mplrcl  14707  uniopn  14724  restbasg  14891  cntop1  14924  cnf  14927  cnpf2  14930  lmtopcnp  14973  psmetdmdm  15047  psmetf  15048  psmet0  15050  xmetf  15073  metf  15074  blhalf  15131  xmetxpbl  15231  ioo2bl  15274  tgioo  15277  cncff  15300  rescncf  15304  cdivcncfap  15327  cnopnap  15334  divcncfap  15337  dedekindeulemeu  15345  dedekindicclemeu  15354  ivthinclemlm  15357  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthinclemdisj  15363  ivthdec  15367  ivthreinc  15368  limcimolemlt  15387  limcimo  15388  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  limccoap  15401  eldvap  15405  dvbsssg  15409  dvfgg  15411  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcj  15432  dvfre  15433  dvrecap  15436  plyco  15482  plycj  15484  sin0pilem1  15504  sin0pilem2  15505  pilem3  15506  tanrpcl  15560  tangtx  15561  perfect  15724  lgsne0  15766  lgseisen  15802  lgsquad2lem2  15810  2sqlem8a  15850  2sqlem8  15851  structgrssvtx  15892  edguhgr  15987  umgrpredgv  15997  umgrnloop2  16001  umgr2edg  16057  subuhgr  16122  subumgr  16124  subusgr  16125  wlkpropg  16174  wlkv  16176  wlkvtxeledgg  16194  wlkvtxiedgg  16196  wlk1walkdom  16209  trlsv  16234  clwwlksswrd  16247  clwwlkclwwlkn  16259  eupthv  16296  eupthseg  16302  nninfalllem1  16610  iooref1o  16638  gfsumval  16680  alsi1d  16692  alsc1d  16694