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  935  3simpa  984  xoror  1369  anxordi  1390  sbidm  1839  reurex  2679  eqimss  3196  eldifi  3244  elinel1  3308  inss1  3342  sopo  4291  wefr  4336  ordtr  4356  opelxp1  4638  relop  4754  funmo  5203  funrel  5205  funinsn  5237  fnfun  5285  ffn  5337  f1f  5393  f1of1  5431  f1ofo  5439  isof1o  5775  eqopi  6140  1st2nd2  6143  reldmtpos  6221  swoer  6529  ecopover  6599  ecopoverg  6602  fnfi  6902  casef  7053  nninff  7087  lpowlpo  7132  dfplpq2  7295  enq0ref  7374  cauappcvgprlemopl  7587  cauappcvgprlemdisj  7592  caucvgprlemopl  7610  caucvgprlemdisj  7615  caucvgprprlemopl  7638  caucvgprprlemopu  7640  caucvgprprlemdisj  7643  peano1nnnn  7793  axrnegex  7820  ltxrlt  7964  1nn  8868  zre  9195  nnssz  9208  ixxss1  9840  ixxss2  9841  ixxss12  9842  iccss2  9880  rge0ssre  9913  elfzuz  9956  uzdisj  10028  nn0disj  10073  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  modfsummodlemstep  11398  mertenslem2  11477  prmnn  12042  prmuz2  12063  oddpwdc  12106  sqpweven  12107  2sqpwodd  12108  phimullem  12157  hashgcdlem  12170  1arith  12297  ctinfom  12361  ctinf  12363  topontop  12652  tpstop  12673  cntop1  12841  cntop2  12842  hmeocn  12945  isxmet2d  12988  metxmet  12995  xmstps  13097  msxms  13098  xmsxmet  13100  msmet  13101  bdxmet  13141  ivthinclemlr  13255  ivthinclemur  13257  bj-indint  13813  bj-inf2vnlem2  13853  peano4nninf  13886