Theorem simplbi 268

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 118	. 2 |- ( ph -> ( ps /\ ch ) )
3	2	simpld 110	1 |- ( ph -> ps )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.62dc  887  3simpa  936  xoror  1311  anxordi  1332  sbidm  1773  reurex  2568  eqimss  3052  eldifi  3095  elinel1  3159  inss1  3193  sopo  4076  wefr  4121  ordtr  4141  opelxp1  4403  relop  4514  funmo  4947  funrel  4949  funinsn  4979  fnfun  5027  ffn  5077  f1f  5123  f1of1  5156  f1ofo  5164  isof1o  5478  eqopi  5829  1st2nd2  5832  reldmtpos  5902  swoer  6200  ecopover  6270  ecopoverg  6273  fnfi  6446  dfplpq2  6606  enq0ref  6685  cauappcvgprlemopl  6898  cauappcvgprlemdisj  6903  caucvgprlemopl  6921  caucvgprlemdisj  6926  caucvgprprlemopl  6949  caucvgprprlemopu  6951  caucvgprprlemdisj  6954  peano1nnnn  7082  axrnegex  7107  ltxrlt  7245  1nn  8117  zre  8436  nnssz  8449  ixxss1  9003  ixxss2  9004  ixxss12  9005  iccss2  9043  rge0ssre  9076  elfzuz  9117  uzdisj  9186  nn0disj  9225  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  prmnn  10636  prmuz2  10656  oddpwdc  10696  sqpweven  10697  2sqpwodd  10698  bj-indint  10884  bj-inf2vnlem2  10924