Theorem simplbi 274

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.62dc  945  3simpa  994  xoror  1379  anxordi  1400  sbidm  1851  reurex  2691  eqimss  3210  eldifi  3258  elinel1  3322  inss1  3356  sopo  4314  wefr  4359  ordtr  4379  opelxp1  4661  relop  4778  funmo  5232  funrel  5234  funinsn  5266  fnfun  5314  ffn  5366  f1f  5422  f1of1  5461  f1ofo  5469  isof1o  5808  eqopi  6173  1st2nd2  6176  reldmtpos  6254  swoer  6563  ecopover  6633  ecopoverg  6636  fnfi  6936  casef  7087  nninff  7121  lpowlpo  7166  dfplpq2  7353  enq0ref  7432  cauappcvgprlemopl  7645  cauappcvgprlemdisj  7650  caucvgprlemopl  7668  caucvgprlemdisj  7673  caucvgprprlemopl  7696  caucvgprprlemopu  7698  caucvgprprlemdisj  7701  peano1nnnn  7851  axrnegex  7878  ltxrlt  8023  1nn  8930  zre  9257  nnssz  9270  ixxss1  9904  ixxss2  9905  ixxss12  9906  iccss2  9944  rge0ssre  9977  elfzuz  10021  uzdisj  10093  nn0disj  10138  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  modfsummodlemstep  11465  mertenslem2  11544  prmnn  12110  prmuz2  12131  oddpwdc  12174  sqpweven  12175  2sqpwodd  12176  phimullem  12225  hashgcdlem  12238  1arith  12365  ctinfom  12429  ctinf  12431  sgrpmgm  12813  mndsgrp  12822  grpmnd  12884  nsgsubg  13065  ablgrp  13093  cmnmnd  13104  crngring  13191  subrgring  13345  subrgrcl  13347  topontop  13517  tpstop  13538  cntop1  13704  cntop2  13705  hmeocn  13808  isxmet2d  13851  metxmet  13858  xmstps  13960  msxms  13961  xmsxmet  13963  msmet  13964  bdxmet  14004  ivthinclemlr  14118  ivthinclemur  14120  bj-indint  14686  bj-inf2vnlem2  14726  peano4nninf  14758