Theorem simplbi 274

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 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 112	1 ⊢ (𝜑 → 𝜓)

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  945  3simpa  994  xoror  1379  anxordi  1400  sbidm  1851  reurex  2691  eqimss  3211  eldifi  3259  elinel1  3323  inss1  3357  sopo  4315  wefr  4360  ordtr  4380  opelxp1  4662  relop  4779  funmo  5233  funrel  5235  funinsn  5267  fnfun  5315  ffn  5367  f1f  5423  f1of1  5462  f1ofo  5470  isof1o  5810  eqopi  6175  1st2nd2  6178  reldmtpos  6256  swoer  6565  ecopover  6635  ecopoverg  6638  fnfi  6938  casef  7089  nninff  7123  lpowlpo  7168  dfplpq2  7355  enq0ref  7434  cauappcvgprlemopl  7647  cauappcvgprlemdisj  7652  caucvgprlemopl  7670  caucvgprlemdisj  7675  caucvgprprlemopl  7698  caucvgprprlemopu  7700  caucvgprprlemdisj  7703  peano1nnnn  7853  axrnegex  7880  ltxrlt  8025  1nn  8932  zre  9259  nnssz  9272  ixxss1  9906  ixxss2  9907  ixxss12  9908  iccss2  9946  rge0ssre  9979  elfzuz  10023  uzdisj  10095  nn0disj  10140  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  modfsummodlemstep  11467  mertenslem2  11546  prmnn  12112  prmuz2  12133  oddpwdc  12176  sqpweven  12177  2sqpwodd  12178  phimullem  12227  hashgcdlem  12240  1arith  12367  ctinfom  12431  ctinf  12433  sgrpmgm  12818  mndsgrp  12827  grpmnd  12889  nsgsubg  13070  ablgrp  13098  cmnmnd  13109  crngring  13196  subrgring  13350  subrgrcl  13352  topontop  13553  tpstop  13574  cntop1  13740  cntop2  13741  hmeocn  13844  isxmet2d  13887  metxmet  13894  xmstps  13996  msxms  13997  xmsxmet  13999  msmet  14000  bdxmet  14040  ivthinclemlr  14154  ivthinclemur  14156  bj-indint  14722  bj-inf2vnlem2  14762  peano4nninf  14794