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  930  3simpa  979  xoror  1358  anxordi  1379  sbidm  1824  reurex  2647  eqimss  3156  eldifi  3203  elinel1  3267  inss1  3301  sopo  4243  wefr  4288  ordtr  4308  opelxp1  4581  relop  4697  funmo  5146  funrel  5148  funinsn  5180  fnfun  5228  ffn  5280  f1f  5336  f1of1  5374  f1ofo  5382  isof1o  5716  eqopi  6078  1st2nd2  6081  reldmtpos  6158  swoer  6465  ecopover  6535  ecopoverg  6538  fnfi  6833  casef  6981  dfplpq2  7186  enq0ref  7265  cauappcvgprlemopl  7478  cauappcvgprlemdisj  7483  caucvgprlemopl  7501  caucvgprlemdisj  7506  caucvgprprlemopl  7529  caucvgprprlemopu  7531  caucvgprprlemdisj  7534  peano1nnnn  7684  axrnegex  7711  ltxrlt  7854  1nn  8755  zre  9082  nnssz  9095  ixxss1  9717  ixxss2  9718  ixxss12  9719  iccss2  9757  rge0ssre  9790  elfzuz  9833  uzdisj  9904  nn0disj  9946  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  modfsummodlemstep  11258  mertenslem2  11337  prmnn  11827  prmuz2  11847  oddpwdc  11888  sqpweven  11889  2sqpwodd  11890  phimullem  11937  hashgcdlem  11939  ctinfom  11977  ctinf  11979  topontop  12220  tpstop  12241  cntop1  12409  cntop2  12410  hmeocn  12513  isxmet2d  12556  metxmet  12563  xmstps  12665  msxms  12666  xmsxmet  12668  msmet  12669  bdxmet  12709  ivthinclemlr  12823  ivthinclemur  12825  bj-indint  13300  bj-inf2vnlem2  13340  nninff  13373  peano4nninf  13375