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  1865  reurex  2715  eqimss  3237  eldifi  3285  elinel1  3349  inss1  3383  sopo  4348  wefr  4393  ordtr  4413  opelxp1  4697  relop  4816  funmo  5273  funrel  5275  funinsn  5307  fnfun  5355  ffn  5407  f1f  5463  f1of1  5503  f1ofo  5511  isof1o  5854  eqopi  6230  1st2nd2  6233  reldmtpos  6311  swoer  6620  ecopover  6692  ecopoverg  6695  fnfi  7002  casef  7154  nninff  7188  lpowlpo  7234  dfplpq2  7421  enq0ref  7500  cauappcvgprlemopl  7713  cauappcvgprlemdisj  7718  caucvgprlemopl  7736  caucvgprlemdisj  7741  caucvgprprlemopl  7764  caucvgprprlemopu  7766  caucvgprprlemdisj  7769  peano1nnnn  7919  axrnegex  7946  ltxrlt  8092  1nn  9001  zre  9330  nnssz  9343  ixxss1  9979  ixxss2  9980  ixxss12  9981  iccss2  10019  rge0ssre  10052  elfzuz  10096  uzdisj  10168  nn0disj  10213  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  0wrd0  10961  modfsummodlemstep  11622  mertenslem2  11701  prmnn  12278  prmuz2  12299  oddpwdc  12342  sqpweven  12343  2sqpwodd  12344  phimullem  12393  hashgcdlem  12406  1arith  12536  ctinfom  12645  ctinf  12647  sgrpmgm  13050  mndsgrp  13062  grpmnd  13139  nsgsubg  13335  ghmgrp1  13375  ghmgrp2  13376  ablgrp  13419  cmnmnd  13431  crngring  13564  rimrhm  13727  subrgring  13780  subrgrcl  13782  rhmpropd  13810  domnnzr  13826  2idlelbas  14072  rng2idlsubgsubrng  14076  2idlcpblrng  14079  2idlcpbl  14080  qusrhm  14084  topontop  14250  tpstop  14271  cntop1  14437  cntop2  14438  hmeocn  14541  isxmet2d  14584  metxmet  14591  xmstps  14693  msxms  14694  xmsxmet  14696  msmet  14697  bdxmet  14737  ivthinclemlr  14873  ivthinclemur  14875  mpodvdsmulf1o  15226  bj-indint  15577  bj-inf2vnlem2  15617  peano4nninf  15650