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  3238  eldifi  3286  elinel1  3350  inss1  3384  sopo  4349  wefr  4394  ordtr  4414  opelxp1  4698  relop  4817  funmo  5274  funrel  5276  funinsn  5308  fnfun  5356  ffn  5410  f1f  5466  f1of1  5506  f1ofo  5514  isof1o  5857  eqopi  6239  1st2nd2  6242  reldmtpos  6320  swoer  6629  ecopover  6701  ecopoverg  6704  fnfi  7011  casef  7163  nninff  7197  lpowlpo  7243  dfplpq2  7438  enq0ref  7517  cauappcvgprlemopl  7730  cauappcvgprlemdisj  7735  caucvgprlemopl  7753  caucvgprlemdisj  7758  caucvgprprlemopl  7781  caucvgprprlemopu  7783  caucvgprprlemdisj  7786  peano1nnnn  7936  axrnegex  7963  ltxrlt  8109  1nn  9018  zre  9347  nnssz  9360  ixxss1  9996  ixxss2  9997  ixxss12  9998  iccss2  10036  rge0ssre  10069  elfzuz  10113  uzdisj  10185  nn0disj  10230  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  0wrd0  10978  modfsummodlemstep  11639  mertenslem2  11718  prmnn  12303  prmuz2  12324  oddpwdc  12367  sqpweven  12368  2sqpwodd  12369  phimullem  12418  hashgcdlem  12431  1arith  12561  ctinfom  12670  ctinf  12672  sgrpmgm  13109  mndsgrp  13123  grpmnd  13209  nsgsubg  13411  ghmgrp1  13451  ghmgrp2  13452  ablgrp  13495  cmnmnd  13507  crngring  13640  rimrhm  13803  subrgring  13856  subrgrcl  13858  rhmpropd  13886  domnnzr  13902  2idlelbas  14148  rng2idlsubgsubrng  14152  2idlcpblrng  14155  2idlcpbl  14156  qusrhm  14160  psr1clfi  14316  topontop  14334  tpstop  14355  cntop1  14521  cntop2  14522  hmeocn  14625  isxmet2d  14668  metxmet  14675  xmstps  14777  msxms  14778  xmsxmet  14780  msmet  14781  bdxmet  14821  ivthinclemlr  14957  ivthinclemur  14959  mpodvdsmulf1o  15310  bj-indint  15661  bj-inf2vnlem2  15701  peano4nninf  15737