Theorem simplbi 272

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi	⊢ (𝜑 → 𝜓)

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 119	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 111	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.62dc  940  3simpa  989  xoror  1374  anxordi  1395  sbidm  1844  reurex  2683  eqimss  3201  eldifi  3249  elinel1  3313  inss1  3347  sopo  4298  wefr  4343  ordtr  4363  opelxp1  4645  relop  4761  funmo  5213  funrel  5215  funinsn  5247  fnfun  5295  ffn  5347  f1f  5403  f1of1  5441  f1ofo  5449  isof1o  5786  eqopi  6151  1st2nd2  6154  reldmtpos  6232  swoer  6541  ecopover  6611  ecopoverg  6614  fnfi  6914  casef  7065  nninff  7099  lpowlpo  7144  dfplpq2  7316  enq0ref  7395  cauappcvgprlemopl  7608  cauappcvgprlemdisj  7613  caucvgprlemopl  7631  caucvgprlemdisj  7636  caucvgprprlemopl  7659  caucvgprprlemopu  7661  caucvgprprlemdisj  7664  peano1nnnn  7814  axrnegex  7841  ltxrlt  7985  1nn  8889  zre  9216  nnssz  9229  ixxss1  9861  ixxss2  9862  ixxss12  9863  iccss2  9901  rge0ssre  9934  elfzuz  9977  uzdisj  10049  nn0disj  10094  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  modfsummodlemstep  11420  mertenslem2  11499  prmnn  12064  prmuz2  12085  oddpwdc  12128  sqpweven  12129  2sqpwodd  12130  phimullem  12179  hashgcdlem  12192  1arith  12319  ctinfom  12383  ctinf  12385  sgrpmgm  12648  mndsgrp  12657  grpmnd  12715  topontop  12806  tpstop  12827  cntop1  12995  cntop2  12996  hmeocn  13099  isxmet2d  13142  metxmet  13149  xmstps  13251  msxms  13252  xmsxmet  13254  msmet  13255  bdxmet  13295  ivthinclemlr  13409  ivthinclemur  13411  bj-indint  13966  bj-inf2vnlem2  14006  peano4nninf  14039