Theorem simplbi 272

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
simplbi	|- ( ph -> ps )

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpi 119	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simpld 111	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.62dc  929  3simpa  978  xoror  1357  anxordi  1378  sbidm  1823  reurex  2644  eqimss  3151  eldifi  3198  elinel1  3262  inss1  3296  sopo  4235  wefr  4280  ordtr  4300  opelxp1  4573  relop  4689  funmo  5138  funrel  5140  funinsn  5172  fnfun  5220  ffn  5272  f1f  5328  f1of1  5366  f1ofo  5374  isof1o  5708  eqopi  6070  1st2nd2  6073  reldmtpos  6150  swoer  6457  ecopover  6527  ecopoverg  6530  fnfi  6825  casef  6973  dfplpq2  7162  enq0ref  7241  cauappcvgprlemopl  7454  cauappcvgprlemdisj  7459  caucvgprlemopl  7477  caucvgprlemdisj  7482  caucvgprprlemopl  7505  caucvgprprlemopu  7507  caucvgprprlemdisj  7510  peano1nnnn  7660  axrnegex  7687  ltxrlt  7830  1nn  8731  zre  9058  nnssz  9071  ixxss1  9687  ixxss2  9688  ixxss12  9689  iccss2  9727  rge0ssre  9760  elfzuz  9802  uzdisj  9873  nn0disj  9915  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  modfsummodlemstep  11226  mertenslem2  11305  prmnn  11791  prmuz2  11811  oddpwdc  11852  sqpweven  11853  2sqpwodd  11854  phimullem  11901  hashgcdlem  11903  ctinfom  11941  ctinf  11943  topontop  12181  tpstop  12202  cntop1  12370  cntop2  12371  hmeocn  12474  isxmet2d  12517  metxmet  12524  xmstps  12626  msxms  12627  xmsxmet  12629  msmet  12630  bdxmet  12670  ivthinclemlr  12784  ivthinclemur  12786  bj-indint  13129  bj-inf2vnlem2  13169  nninff  13198  peano4nninf  13200