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  3177  unssad  3350  opth1  4280  opth  4281  0nelop  4292  epelg  4337  poirr  4354  brrelex1  4714  brrelex  4715  asymref  5068  soirri  5077  sotri  5078  fcnvres  5459  fun11iun  5543  funopsn  5762  elmpocl1  6142  f1od  6149  f1o2d  6151  oprssdmm  6257  smoiso  6388  tfrlem1  6394  swoer  6648  ecopovtrn  6719  ecopovtrng  6722  elmapssres  6760  pmresg  6763  mapsspm  6769  en1uniel  6896  pw2f1odc  6932  xpf1o  6941  sbthlemi9  7067  supelti  7104  supsnti  7107  supisoti  7112  ctssdccl  7213  ctfoex  7220  fodjum  7248  en2eleq  7303  djuen  7323  dftap2  7363  2omotaplemst  7370  exmidapne  7372  ccfunen  7376  dfplpq2  7467  ltbtwnnqq  7528  enq0tr  7547  elnp1st2nd  7589  prcdnql  7597  prnminu  7602  prloc  7604  genpcdl  7632  addnqprulem  7641  addlocprlemlt  7644  addlocprlemgt  7647  addlocprlem  7648  addlocpr  7649  nqprxx  7659  ltnqex  7662  addnqprlemfl  7672  addnqprlemfu  7673  appdivnq  7676  prmuloclemcalc  7678  prmuloc  7679  mullocprlem  7683  mulnqprlemfl  7688  mulnqprlemfu  7689  ltprordil  7702  ltnqpri  7707  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  ltexpri  7726  lteupri  7730  ltaprlem  7731  recexprlemell  7735  recexprlemelu  7736  recexprlemloc  7744  recexprlempr  7745  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1u  7749  aptipr  7754  cauappcvgprlemm  7758  cauappcvgprlemlol  7760  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  cauappcvgprlem1  7772  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemlol  7783  caucvgprlemladdfu  7790  caucvgprprlemloccalc  7797  caucvgprprlemnkltj  7802  caucvgprprlemnbj  7806  caucvgprprlemml  7807  caucvgprprlemlol  7811  caucvgprprlemloc  7816  caucvgprprlemexbt  7819  suplocexprlemss  7828  suplocexprlemru  7832  suplocexprlemlub  7837  ltsrprg  7860  caucvgsrlemasr  7903  suplocsrlemb  7919  suplocsrlem  7921  suplocsr  7922  axcaucvglemcau  8011  axpre-suploclemres  8014  negf1o  8454  apreap  8660  apreim  8676  msqge0  8689  mulge0  8692  apti  8695  apsscn  8720  mulap0bad  8732  divadddivap  8800  recnz  9466  lbzbi  9737  xadd4d  10007  ixxss1  10026  ixxss2  10027  ixxss12  10028  iccss2  10066  iccssioo2  10068  iccssico2  10069  iccen  10128  elfzole1  10278  ioom  10403  elicore  10409  flqle  10421  flqltnz  10430  addmodlteq  10543  expclzap  10709  hashennnuni  10924  zfz1isolem1  10985  hashdmprop2dom  10989  swrdsbslen  11119  ccatswrd  11123  recl  11164  cvg1nlemcau  11295  cvg1nlemres  11296  resqrtth  11342  fimaxre2  11538  climcl  11593  reccn2ap  11624  nnf1o  11687  summodclem3  11691  sumpr  11724  fsump1i  11744  fisumcom2  11749  fsum00  11773  fsumparts  11781  mertenslemi1  11846  prodmodclem3  11886  fprodcom2fi  11937  addsin  12053  subsin  12054  addcos  12057  subcos  12058  sinbnd2  12065  cosbnd2  12066  sin01gt0  12073  cos01gt0  12074  divgcdz  12292  divgcdnn  12296  gcdaddm  12305  bezoutlemstep  12318  dvdsgcdb  12334  dfgcd2  12335  mulgcd  12337  gcdzeq  12343  dvdsmulgcd  12346  sqgcd  12350  bezoutr  12353  lcmval  12385  lcmcllem  12389  gcddvdslcm  12395  lcmgcdlem  12399  lcmgcd  12400  lcmgcdeq  12405  lcmdvdsb  12406  mulgcddvds  12416  rpmulgcd2  12417  qredeu  12419  rpdvds  12421  isprm3  12440  divgcdodd  12465  coprm  12466  rpexp  12475  sqrt2irr  12484  qnumcl  12510  qnumdencoprm  12515  divnumden  12518  numsq  12525  phimullem  12547  eulerthlem1  12549  prmdiveq  12558  prmdivdiv  12559  hashgcdlem  12560  odzcl  12566  reumodprminv  12576  pythagtriplem19  12605  pclemub  12610  pcprendvds  12613  pcprendvds2  12614  pcpre1  12615  pcpremul  12616  pceulem  12617  pceu  12618  pczpre  12620  pczcl  12621  pcgcd1  12651  pc2dvds  12653  pcaddlem  12662  pcmpt  12666  pockthlem  12679  prmunb  12685  4sqlem7  12707  4sqlem8  12708  4sqlem9  12709  4sqlem10  12710  4sqlem14  12727  4sqlem15  12728  4sqlem16  12729  4sqlem17  12730  4sqlem18  12731  ennnfonelemg  12774  ennnfonelemf1  12789  ctiunctlemu1st  12805  nninfdclemf  12820  nninfdclemp1  12821  mgmidcl  13210  gsumfzval  13223  gsumval2  13229  mndlid  13267  prdsmndd  13280  imasmndf1  13286  dfgrp3mlem  13430  grplactf1o  13435  prdsgrpd  13441  prdsinvgd  13442  imasgrpf1  13448  subgsubm  13532  qusgrp  13568  ghmgrp1  13581  ghmf  13583  ghmnsgpreima  13605  kerf1ghm  13610  conjsubg  13613  imasrng  13718  srgdilem  13731  srgdi  13736  srglidm  13741  ringdilem  13774  ringdi  13780  ringlidm  13785  imasring  13826  imasringf1  13827  dvdsrcld  13859  unitcld  13870  unitmulcl  13875  unitnegcl  13892  rhmghm  13924  elrhmunit  13939  subrgss  13984  subrgrcl  13988  lmodvscl  14067  lmodvsdi  14073  lmodvsdir  14074  lsslsp  14191  qusring  14289  crngridl  14292  znunit  14421  znrrg  14422  psrbaglesuppg  14434  psrelbas  14437  psraddcl  14442  mplrcl  14456  uniopn  14473  restbasg  14640  cntop1  14673  cnf  14676  cnpf2  14679  lmtopcnp  14722  psmetdmdm  14796  psmetf  14797  psmet0  14799  xmetf  14822  metf  14823  blhalf  14880  xmetxpbl  14980  ioo2bl  15023  tgioo  15026  cncff  15049  rescncf  15053  cdivcncfap  15076  cnopnap  15083  divcncfap  15086  dedekindeulemeu  15094  dedekindicclemeu  15103  ivthinclemlm  15106  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthinclemdisj  15112  ivthdec  15116  ivthreinc  15117  limcimolemlt  15136  limcimo  15137  limccnpcntop  15147  limccnp2lem  15148  limccnp2cntop  15149  limccoap  15150  eldvap  15154  dvbsssg  15158  dvfgg  15160  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcj  15181  dvfre  15182  dvrecap  15185  plyco  15231  plycj  15233  sin0pilem1  15253  sin0pilem2  15254  pilem3  15255  tanrpcl  15309  tangtx  15310  perfect  15473  lgsne0  15515  lgseisen  15551  lgsquad2lem2  15559  2sqlem8a  15599  2sqlem8  15600  structgrssvtx  15639  nninfalllem1  15945  iooref1o  15973  alsi1d  16020  alsc1d  16022