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:  bi1  117  simplbi  272  simprbda  381  simp1  982  eldifad  3087  unssad  3258  opth1  4166  opth  4167  0nelop  4178  epelg  4220  poirr  4237  brrelex1  4586  brrelex  4587  asymref  4932  soirri  4941  sotri  4942  fcnvres  5314  fun11iun  5396  elmpocl1  5977  f1od  5981  f1o2d  5983  oprssdmm  6077  smoiso  6207  tfrlem1  6213  swoer  6465  ecopovtrn  6534  ecopovtrng  6537  elmapssres  6575  pmresg  6578  mapsspm  6584  en1uniel  6706  xpf1o  6746  sbthlemi9  6861  supelti  6897  supsnti  6900  supisoti  6905  ctssdccl  7004  ctfoex  7011  fodjum  7026  en2eleq  7068  djuen  7084  ccfunen  7096  dfplpq2  7186  ltbtwnnqq  7247  enq0tr  7266  elnp1st2nd  7308  prcdnql  7316  prnminu  7321  prloc  7323  genpcdl  7351  addnqprulem  7360  addlocprlemlt  7363  addlocprlemgt  7366  addlocprlem  7367  addlocpr  7368  nqprxx  7378  ltnqex  7381  addnqprlemfl  7391  addnqprlemfu  7392  appdivnq  7395  prmuloclemcalc  7397  prmuloc  7398  mullocprlem  7402  mulnqprlemfl  7407  mulnqprlemfu  7408  ltprordil  7421  ltnqpri  7426  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  ltexpri  7445  lteupri  7449  ltaprlem  7450  recexprlemell  7454  recexprlemelu  7455  recexprlemloc  7463  recexprlempr  7464  recexprlem1ssl  7465  recexprlem1ssu  7466  recexprlemss1u  7468  aptipr  7473  cauappcvgprlemm  7477  cauappcvgprlemlol  7479  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlem1  7491  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemlol  7502  caucvgprlemladdfu  7509  caucvgprprlemloccalc  7516  caucvgprprlemnkltj  7521  caucvgprprlemnbj  7525  caucvgprprlemml  7526  caucvgprprlemlol  7530  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  suplocexprlemss  7547  suplocexprlemru  7551  suplocexprlemlub  7556  ltsrprg  7579  caucvgsrlemasr  7622  suplocsrlemb  7638  suplocsrlem  7640  suplocsr  7641  axcaucvglemcau  7730  axpre-suploclemres  7733  negf1o  8168  apreap  8373  apreim  8389  msqge0  8402  mulge0  8405  apti  8408  apsscn  8433  mulap0bad  8444  divadddivap  8511  recnz  9168  lbzbi  9435  xadd4d  9698  ixxss1  9717  ixxss2  9718  ixxss12  9719  iccss2  9757  iccssioo2  9759  iccssico2  9760  iccen  9819  elfzole1  9963  ioom  10069  flqle  10082  flqltnz  10091  addmodlteq  10202  expclzap  10349  hashennnuni  10557  zfz1isolem1  10615  recl  10657  cvg1nlemcau  10788  cvg1nlemres  10789  resqrtth  10835  fimaxre2  11030  climcl  11083  reccn2ap  11114  nnf1o  11177  summodclem3  11181  sumpr  11214  fsump1i  11234  fisumcom2  11239  fsum00  11263  fsumparts  11271  mertenslemi1  11336  prodmodclem3  11376  addsin  11485  subsin  11486  addcos  11489  subcos  11490  sinbnd2  11497  cosbnd2  11498  sin01gt0  11504  cos01gt0  11505  divgcdz  11696  divgcdnn  11699  gcdaddm  11708  bezoutlemstep  11721  dvdsgcdb  11737  dfgcd2  11738  mulgcd  11740  gcdzeq  11746  dvdsmulgcd  11749  sqgcd  11753  bezoutr  11756  lcmval  11780  lcmcllem  11784  gcddvdslcm  11790  lcmgcdlem  11794  lcmgcd  11795  lcmgcdeq  11800  lcmdvdsb  11801  mulgcddvds  11811  rpmulgcd2  11812  qredeu  11814  rpdvds  11816  isprm3  11835  divgcdodd  11857  coprm  11858  rpexp  11867  sqrt2irr  11876  qnumcl  11902  qnumdencoprm  11907  divnumden  11910  numsq  11917  phimullem  11937  hashgcdlem  11939  ennnfonelemg  11952  ennnfonelemf1  11967  ctiunctlemu1st  11983  uniopn  12207  restbasg  12376  cntop1  12409  cnf  12412  cnpf2  12415  lmtopcnp  12458  psmetdmdm  12532  psmetf  12533  psmet0  12535  xmetf  12558  metf  12559  blhalf  12616  xmetxpbl  12716  ioo2bl  12751  tgioo  12754  cncff  12772  rescncf  12776  cdivcncfap  12795  cnopnap  12802  dedekindeulemeu  12808  dedekindicclemeu  12817  ivthinclemlm  12820  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthinclemdisj  12826  ivthdec  12830  limcimolemlt  12841  limcimo  12842  limccnpcntop  12852  limccnp2lem  12853  limccnp2cntop  12854  limccoap  12855  eldvap  12859  dvbsssg  12863  dvfgg  12865  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcj  12881  dvfre  12882  dvrecap  12885  sin0pilem1  12910  sin0pilem2  12911  pilem3  12912  tanrpcl  12966  tangtx  12967  nninfalllem1  13378  iooref1o  13426  alsi1d  13438  alsc1d  13440