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  11251  ccatswrd  11255  ccatpfx  11286  recl  11431  cvg1nlemcau  11562  cvg1nlemres  11563  resqrtth  11609  fimaxre2  11805  climcl  11860  reccn2ap  11891  nnf1o  11955  summodclem3  11959  sumpr  11992  fsump1i  12012  fisumcom2  12017  fsum00  12041  fsumparts  12049  mertenslemi1  12114  prodmodclem3  12154  fprodcom2fi  12205  addsin  12321  subsin  12322  addcos  12325  subcos  12326  sinbnd2  12333  cosbnd2  12334  sin01gt0  12341  cos01gt0  12342  divgcdz  12560  divgcdnn  12564  gcdaddm  12573  bezoutlemstep  12586  dvdsgcdb  12602  dfgcd2  12603  mulgcd  12605  gcdzeq  12611  dvdsmulgcd  12614  sqgcd  12618  bezoutr  12621  lcmval  12653  lcmcllem  12657  gcddvdslcm  12663  lcmgcdlem  12667  lcmgcd  12668  lcmgcdeq  12673  lcmdvdsb  12674  mulgcddvds  12684  rpmulgcd2  12685  qredeu  12687  rpdvds  12689  isprm3  12708  divgcdodd  12733  coprm  12734  rpexp  12743  sqrt2irr  12752  qnumcl  12778  qnumdencoprm  12783  divnumden  12786  numsq  12793  phimullem  12815  eulerthlem1  12817  prmdiveq  12826  prmdivdiv  12827  hashgcdlem  12828  odzcl  12834  reumodprminv  12844  pythagtriplem19  12873  pclemub  12878  pcprendvds  12881  pcprendvds2  12882  pcpre1  12883  pcpremul  12884  pceulem  12885  pceu  12886  pczpre  12888  pczcl  12889  pcgcd1  12919  pc2dvds  12921  pcaddlem  12930  pcmpt  12934  pockthlem  12947  prmunb  12953  4sqlem7  12975  4sqlem8  12976  4sqlem9  12977  4sqlem10  12978  4sqlem14  12995  4sqlem15  12996  4sqlem16  12997  4sqlem17  12998  4sqlem18  12999  ennnfonelemg  13042  ennnfonelemf1  13057  ctiunctlemu1st  13073  nninfdclemf  13088  nninfdclemp1  13089  mgmidcl  13479  gsumfzval  13492  gsumval2  13498  mndlid  13536  prdsmndd  13549  imasmndf1  13555  dfgrp3mlem  13699  grplactf1o  13704  prdsgrpd  13710  prdsinvgd  13711  imasgrpf1  13717  subgsubm  13801  qusgrp  13837  ghmgrp1  13850  ghmf  13852  ghmnsgpreima  13874  kerf1ghm  13879  conjsubg  13882  gsumsplit0  13951  imasrng  13988  srgdilem  14001  srgdi  14006  srglidm  14011  ringdilem  14044  ringdi  14050  ringlidm  14055  imasring  14096  imasringf1  14097  dvdsrcld  14130  unitcld  14141  unitmulcl  14146  unitnegcl  14163  rhmghm  14195  elrhmunit  14210  subrgss  14255  subrgrcl  14259  lmodvscl  14338  lmodvsdi  14344  lmodvsdir  14345  lsslsp  14462  qusring  14560  crngridl  14563  znunit  14692  znrrg  14693  psrbaglesuppg  14705  psrelbas  14708  psraddcl  14713  mplrcl  14727  uniopn  14744  restbasg  14911  cntop1  14944  cnf  14947  cnpf2  14950  lmtopcnp  14993  psmetdmdm  15067  psmetf  15068  psmet0  15070  xmetf  15093  metf  15094  blhalf  15151  xmetxpbl  15251  ioo2bl  15294  tgioo  15297  cncff  15320  rescncf  15324  cdivcncfap  15347  cnopnap  15354  divcncfap  15357  dedekindeulemeu  15365  dedekindicclemeu  15374  ivthinclemlm  15377  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthinclemdisj  15383  ivthdec  15387  ivthreinc  15388  limcimolemlt  15407  limcimo  15408  limccnpcntop  15418  limccnp2lem  15419  limccnp2cntop  15420  limccoap  15421  eldvap  15425  dvbsssg  15429  dvfgg  15431  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcj  15452  dvfre  15453  dvrecap  15456  plyco  15502  plycj  15504  sin0pilem1  15524  sin0pilem2  15525  pilem3  15526  tanrpcl  15580  tangtx  15581  perfect  15744  lgsne0  15786  lgseisen  15822  lgsquad2lem2  15830  2sqlem8a  15870  2sqlem8  15871  structgrssvtx  15912  edguhgr  16007  umgrpredgv  16017  umgrnloop2  16021  umgr2edg  16077  subuhgr  16142  subumgr  16144  subusgr  16145  wlkpropg  16194  wlkv  16196  wlkvtxeledgg  16214  wlkvtxiedgg  16216  wlk1walkdom  16229  trlsv  16254  clwwlksswrd  16267  clwwlkclwwlkn  16279  eupthv  16316  eupthseg  16322  eupth2lem3lem3fi  16340  eupth2lem3lem4fi  16343  eupth2lemsfi  16348  eulerpathprum  16350  nninfalllem1  16661  iooref1o  16689  gfsumval  16732  alsi1d  16747  alsc1d  16749