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  1398  anxordi  1419  sbidm  1873  reurex  2723  eqimss  3246  eldifi  3294  elinel1  3358  inss1  3392  sopo  4359  wefr  4404  ordtr  4424  opelxp1  4708  relop  4827  funmo  5285  funrel  5287  funinsn  5322  fnfun  5370  ffn  5424  f1f  5480  f1of1  5520  f1ofo  5528  isof1o  5875  eqopi  6257  1st2nd2  6260  reldmtpos  6338  swoer  6647  ecopover  6719  ecopoverg  6722  fnfi  7037  casef  7189  nninff  7223  lpowlpo  7269  dfplpq2  7466  enq0ref  7545  cauappcvgprlemopl  7758  cauappcvgprlemdisj  7763  caucvgprlemopl  7781  caucvgprlemdisj  7786  caucvgprprlemopl  7809  caucvgprprlemopu  7811  caucvgprprlemdisj  7814  peano1nnnn  7964  axrnegex  7991  ltxrlt  8137  1nn  9046  zre  9375  nnssz  9388  ixxss1  10025  ixxss2  10026  ixxss12  10027  iccss2  10065  rge0ssre  10098  elfzuz  10142  uzdisj  10214  nn0disj  10259  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  0wrd0  11018  modfsummodlemstep  11739  mertenslem2  11818  prmnn  12403  prmuz2  12424  oddpwdc  12467  sqpweven  12468  2sqpwodd  12469  phimullem  12518  hashgcdlem  12531  1arith  12661  ctinfom  12770  ctinf  12772  sgrpmgm  13210  mndsgrp  13224  grpmnd  13310  nsgsubg  13512  ghmgrp1  13552  ghmgrp2  13553  ablgrp  13596  cmnmnd  13608  crngring  13741  rimrhm  13904  subrgring  13957  subrgrcl  13959  rhmpropd  13987  domnnzr  14003  2idlelbas  14249  rng2idlsubgsubrng  14253  2idlcpblrng  14256  2idlcpbl  14257  qusrhm  14261  psr1clfi  14421  topontop  14457  tpstop  14478  cntop1  14644  cntop2  14645  hmeocn  14748  isxmet2d  14791  metxmet  14798  xmstps  14900  msxms  14901  xmsxmet  14903  msmet  14904  bdxmet  14944  ivthinclemlr  15080  ivthinclemur  15082  mpodvdsmulf1o  15433  bj-indint  15829  bj-inf2vnlem2  15869  peano4nninf  15905