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  947  3simpa  996  xoror  1390  anxordi  1411  sbidm  1862  reurex  2712  eqimss  3234  eldifi  3282  elinel1  3346  inss1  3380  sopo  4345  wefr  4390  ordtr  4410  opelxp1  4694  relop  4813  funmo  5270  funrel  5272  funinsn  5304  fnfun  5352  ffn  5404  f1f  5460  f1of1  5500  f1ofo  5508  isof1o  5851  eqopi  6227  1st2nd2  6230  reldmtpos  6308  swoer  6617  ecopover  6689  ecopoverg  6692  fnfi  6997  casef  7149  nninff  7183  lpowlpo  7229  dfplpq2  7416  enq0ref  7495  cauappcvgprlemopl  7708  cauappcvgprlemdisj  7713  caucvgprlemopl  7731  caucvgprlemdisj  7736  caucvgprprlemopl  7759  caucvgprprlemopu  7761  caucvgprprlemdisj  7764  peano1nnnn  7914  axrnegex  7941  ltxrlt  8087  1nn  8995  zre  9324  nnssz  9337  ixxss1  9973  ixxss2  9974  ixxss12  9975  iccss2  10013  rge0ssre  10046  elfzuz  10090  uzdisj  10162  nn0disj  10207  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  0wrd0  10943  modfsummodlemstep  11603  mertenslem2  11682  prmnn  12251  prmuz2  12272  oddpwdc  12315  sqpweven  12316  2sqpwodd  12317  phimullem  12366  hashgcdlem  12379  1arith  12508  ctinfom  12588  ctinf  12590  sgrpmgm  12993  mndsgrp  13005  grpmnd  13082  nsgsubg  13278  ghmgrp1  13318  ghmgrp2  13319  ablgrp  13362  cmnmnd  13374  crngring  13507  rimrhm  13670  subrgring  13723  subrgrcl  13725  rhmpropd  13753  domnnzr  13769  2idlelbas  14015  rng2idlsubgsubrng  14019  2idlcpblrng  14022  2idlcpbl  14023  qusrhm  14027  topontop  14193  tpstop  14214  cntop1  14380  cntop2  14381  hmeocn  14484  isxmet2d  14527  metxmet  14534  xmstps  14636  msxms  14637  xmsxmet  14639  msmet  14640  bdxmet  14680  ivthinclemlr  14816  ivthinclemur  14818  bj-indint  15493  bj-inf2vnlem2  15533  peano4nninf  15566