Theorem simpld 111

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem is referenced by:  biimp  117  simplbi  272  simprbda  381  simp1  987  eldifad  3126  unssad  3298  opth1  4213  opth  4214  0nelop  4225  epelg  4267  poirr  4284  brrelex1  4642  brrelex  4643  asymref  4988  soirri  4997  sotri  4998  fcnvres  5370  fun11iun  5452  elmpocl1  6036  f1od  6040  f1o2d  6042  oprssdmm  6136  smoiso  6266  tfrlem1  6272  swoer  6525  ecopovtrn  6594  ecopovtrng  6597  elmapssres  6635  pmresg  6638  mapsspm  6644  en1uniel  6766  xpf1o  6806  sbthlemi9  6926  supelti  6963  supsnti  6966  supisoti  6971  ctssdccl  7072  ctfoex  7079  fodjum  7106  en2eleq  7147  djuen  7163  ccfunen  7201  dfplpq2  7291  ltbtwnnqq  7352  enq0tr  7371  elnp1st2nd  7413  prcdnql  7421  prnminu  7426  prloc  7428  genpcdl  7456  addnqprulem  7465  addlocprlemlt  7468  addlocprlemgt  7471  addlocprlem  7472  addlocpr  7473  nqprxx  7483  ltnqex  7486  addnqprlemfl  7496  addnqprlemfu  7497  appdivnq  7500  prmuloclemcalc  7502  prmuloc  7503  mullocprlem  7507  mulnqprlemfl  7512  mulnqprlemfu  7513  ltprordil  7526  ltnqpri  7531  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemlol  7539  ltexprlemopu  7540  ltexprlemupu  7541  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemfl  7546  ltexprlemrl  7547  ltexprlemfu  7548  ltexprlemru  7549  ltexpri  7550  lteupri  7554  ltaprlem  7555  recexprlemell  7559  recexprlemelu  7560  recexprlemloc  7568  recexprlempr  7569  recexprlem1ssl  7570  recexprlem1ssu  7571  recexprlemss1u  7573  aptipr  7578  cauappcvgprlemm  7582  cauappcvgprlemlol  7584  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlem1  7596  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemlol  7607  caucvgprlemladdfu  7614  caucvgprprlemloccalc  7621  caucvgprprlemnkltj  7626  caucvgprprlemnbj  7630  caucvgprprlemml  7631  caucvgprprlemlol  7635  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  suplocexprlemss  7652  suplocexprlemru  7656  suplocexprlemlub  7661  ltsrprg  7684  caucvgsrlemasr  7727  suplocsrlemb  7743  suplocsrlem  7745  suplocsr  7746  axcaucvglemcau  7835  axpre-suploclemres  7838  negf1o  8276  apreap  8481  apreim  8497  msqge0  8510  mulge0  8513  apti  8516  apsscn  8541  mulap0bad  8552  divadddivap  8619  recnz  9280  lbzbi  9550  xadd4d  9817  ixxss1  9836  ixxss2  9837  ixxss12  9838  iccss2  9876  iccssioo2  9878  iccssico2  9879  iccen  9938  elfzole1  10086  ioom  10192  elicore  10198  flqle  10209  flqltnz  10218  addmodlteq  10329  expclzap  10476  hashennnuni  10688  zfz1isolem1  10749  recl  10791  cvg1nlemcau  10922  cvg1nlemres  10923  resqrtth  10969  fimaxre2  11164  climcl  11219  reccn2ap  11250  nnf1o  11313  summodclem3  11317  sumpr  11350  fsump1i  11370  fisumcom2  11375  fsum00  11399  fsumparts  11407  mertenslemi1  11472  prodmodclem3  11512  fprodcom2fi  11563  addsin  11679  subsin  11680  addcos  11683  subcos  11684  sinbnd2  11691  cosbnd2  11692  sin01gt0  11698  cos01gt0  11699  divgcdz  11900  divgcdnn  11904  gcdaddm  11913  bezoutlemstep  11926  dvdsgcdb  11942  dfgcd2  11943  mulgcd  11945  gcdzeq  11951  dvdsmulgcd  11954  sqgcd  11958  bezoutr  11961  lcmval  11991  lcmcllem  11995  gcddvdslcm  12001  lcmgcdlem  12005  lcmgcd  12006  lcmgcdeq  12011  lcmdvdsb  12012  mulgcddvds  12022  rpmulgcd2  12023  qredeu  12025  rpdvds  12027  isprm3  12046  divgcdodd  12071  coprm  12072  rpexp  12081  sqrt2irr  12090  qnumcl  12116  qnumdencoprm  12121  divnumden  12124  numsq  12131  phimullem  12153  eulerthlem1  12155  prmdiveq  12164  prmdivdiv  12165  hashgcdlem  12166  odzcl  12171  reumodprminv  12181  pythagtriplem19  12210  pclemub  12215  pcprendvds  12218  pcprendvds2  12219  pcpre1  12220  pcpremul  12221  pceulem  12222  pceu  12223  pczpre  12225  pczcl  12226  pcgcd1  12255  pc2dvds  12257  pcaddlem  12266  pcmpt  12269  pockthlem  12282  prmunb  12288  4sqlem7  12310  4sqlem8  12311  4sqlem9  12312  4sqlem10  12313  ennnfonelemg  12332  ennnfonelemf1  12347  ctiunctlemu1st  12363  nninfdclemf  12378  nninfdclemp1  12379  uniopn  12599  restbasg  12768  cntop1  12801  cnf  12804  cnpf2  12807  lmtopcnp  12850  psmetdmdm  12924  psmetf  12925  psmet0  12927  xmetf  12950  metf  12951  blhalf  13008  xmetxpbl  13108  ioo2bl  13143  tgioo  13146  cncff  13164  rescncf  13168  cdivcncfap  13187  cnopnap  13194  dedekindeulemeu  13200  dedekindicclemeu  13209  ivthinclemlm  13212  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthinclemdisj  13218  ivthdec  13222  limcimolemlt  13233  limcimo  13234  limccnpcntop  13244  limccnp2lem  13245  limccnp2cntop  13246  limccoap  13247  eldvap  13251  dvbsssg  13255  dvfgg  13257  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcj  13273  dvfre  13274  dvrecap  13277  sin0pilem1  13302  sin0pilem2  13303  pilem3  13304  tanrpcl  13358  tangtx  13359  lgsne0  13539  2sqlem8a  13558  2sqlem8  13559  nninfalllem1  13848  iooref1o  13873  alsi1d  13917  alsc1d  13919