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:  an3  589  pm5.62dc  951  3simpa  1018  xoror  1421  anxordi  1442  sbidm  1897  reurex  2750  eqimss  3278  eldifi  3326  elinel1  3390  inss1  3424  sopo  4404  wefr  4449  ordtr  4469  opelxp1  4753  relop  4872  ssrelrn  4914  funmo  5333  funrel  5335  funinsn  5370  fnfun  5418  ffn  5473  f1f  5533  f1of1  5573  f1ofo  5581  isof1o  5937  eqopi  6324  1st2nd2  6327  reldmtpos  6405  swoer  6716  ecopover  6788  ecopoverg  6791  fnfi  7114  casef  7266  nninff  7300  lpowlpo  7346  dfplpq2  7552  enq0ref  7631  cauappcvgprlemopl  7844  cauappcvgprlemdisj  7849  caucvgprlemopl  7867  caucvgprlemdisj  7872  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemdisj  7900  peano1nnnn  8050  axrnegex  8077  ltxrlt  8223  1nn  9132  zre  9461  nnssz  9474  ixxss1  10112  ixxss2  10113  ixxss12  10114  iccss2  10152  rge0ssre  10185  elfzuz  10229  uzdisj  10301  nn0disj  10346  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  0wrd0  11110  modfsummodlemstep  11983  mertenslem2  12062  prmnn  12647  prmuz2  12668  oddpwdc  12711  sqpweven  12712  2sqpwodd  12713  phimullem  12762  hashgcdlem  12775  1arith  12905  ctinfom  13014  ctinf  13016  sgrpmgm  13455  mndsgrp  13469  grpmnd  13555  nsgsubg  13757  ghmgrp1  13797  ghmgrp2  13798  ablgrp  13841  cmnmnd  13853  crngring  13986  rimrhm  14150  subrgring  14203  subrgrcl  14205  rhmpropd  14233  domnnzr  14249  2idlelbas  14495  rng2idlsubgsubrng  14499  2idlcpblrng  14502  2idlcpbl  14503  qusrhm  14507  psr1clfi  14667  topontop  14703  tpstop  14724  cntop1  14890  cntop2  14891  hmeocn  14994  isxmet2d  15037  metxmet  15044  xmstps  15146  msxms  15147  xmsxmet  15149  msmet  15150  bdxmet  15190  ivthinclemlr  15326  ivthinclemur  15328  mpodvdsmulf1o  15679  uhgr0vb  15899  trliswlk  16125  bj-indint  16349  bj-inf2vnlem2  16389  peano4nninf  16432