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  891  3simpa  940  xoror  1315  anxordi  1336  sbidm  1779  reurex  2580  eqimss  3078  eldifi  3122  elinel1  3186  inss1  3220  sopo  4140  wefr  4185  ordtr  4205  opelxp1  4471  relop  4586  funmo  5030  funrel  5032  funinsn  5063  fnfun  5111  ffn  5161  f1f  5216  f1of1  5252  f1ofo  5260  isof1o  5586  eqopi  5942  1st2nd2  5945  reldmtpos  6018  swoer  6318  ecopover  6388  ecopoverg  6391  fnfi  6644  casef  6777  dfplpq2  6911  enq0ref  6990  cauappcvgprlemopl  7203  cauappcvgprlemdisj  7208  caucvgprlemopl  7226  caucvgprlemdisj  7231  caucvgprprlemopl  7254  caucvgprprlemopu  7256  caucvgprprlemdisj  7259  peano1nnnn  7387  axrnegex  7412  ltxrlt  7550  1nn  8431  zre  8752  nnssz  8765  ixxss1  9320  ixxss2  9321  ixxss12  9322  iccss2  9360  rge0ssre  9393  elfzuz  9434  uzdisj  9503  nn0disj  9545  frecuzrdgtcl  9815  frecuzrdgfunlem  9822  modfsummodlemstep  10847  mertenslem2  10926  prmnn  11366  prmuz2  11386  oddpwdc  11426  sqpweven  11427  2sqpwodd  11428  phimullem  11475  hashgcdlem  11477  topontop  11566  bj-indint  11781  bj-inf2vnlem2  11821  nninff  11849  peano4nninf  11851