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  11710  mertenslem2  11789  prmnn  12374  prmuz2  12395  oddpwdc  12438  sqpweven  12439  2sqpwodd  12440  phimullem  12489  hashgcdlem  12502  1arith  12632  ctinfom  12741  ctinf  12743  sgrpmgm  13181  mndsgrp  13195  grpmnd  13281  nsgsubg  13483  ghmgrp1  13523  ghmgrp2  13524  ablgrp  13567  cmnmnd  13579  crngring  13712  rimrhm  13875  subrgring  13928  subrgrcl  13930  rhmpropd  13958  domnnzr  13974  2idlelbas  14220  rng2idlsubgsubrng  14224  2idlcpblrng  14227  2idlcpbl  14228  qusrhm  14232  psr1clfi  14392  topontop  14428  tpstop  14449  cntop1  14615  cntop2  14616  hmeocn  14719  isxmet2d  14762  metxmet  14769  xmstps  14871  msxms  14872  xmsxmet  14874  msmet  14875  bdxmet  14915  ivthinclemlr  15051  ivthinclemur  15053  mpodvdsmulf1o  15404  bj-indint  15800  bj-inf2vnlem2  15840  peano4nninf  15876