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  2690  eqimss  3209  eldifi  3257  elinel1  3321  inss1  3355  sopo  4313  wefr  4358  ordtr  4378  opelxp1  4660  relop  4777  funmo  5231  funrel  5233  funinsn  5265  fnfun  5313  ffn  5365  f1f  5421  f1of1  5460  f1ofo  5468  isof1o  5807  eqopi  6172  1st2nd2  6175  reldmtpos  6253  swoer  6562  ecopover  6632  ecopoverg  6635  fnfi  6935  casef  7086  nninff  7120  lpowlpo  7165  dfplpq2  7352  enq0ref  7431  cauappcvgprlemopl  7644  cauappcvgprlemdisj  7649  caucvgprlemopl  7667  caucvgprlemdisj  7672  caucvgprprlemopl  7695  caucvgprprlemopu  7697  caucvgprprlemdisj  7700  peano1nnnn  7850  axrnegex  7877  ltxrlt  8022  1nn  8929  zre  9256  nnssz  9269  ixxss1  9903  ixxss2  9904  ixxss12  9905  iccss2  9943  rge0ssre  9976  elfzuz  10020  uzdisj  10092  nn0disj  10137  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  modfsummodlemstep  11464  mertenslem2  11543  prmnn  12109  prmuz2  12130  oddpwdc  12173  sqpweven  12174  2sqpwodd  12175  phimullem  12224  hashgcdlem  12237  1arith  12364  ctinfom  12428  ctinf  12430  sgrpmgm  12812  mndsgrp  12821  grpmnd  12883  nsgsubg  13063  ablgrp  13091  cmnmnd  13102  crngring  13189  subrgring  13343  subrgrcl  13345  topontop  13484  tpstop  13505  cntop1  13671  cntop2  13672  hmeocn  13775  isxmet2d  13818  metxmet  13825  xmstps  13927  msxms  13928  xmsxmet  13930  msmet  13931  bdxmet  13971  ivthinclemlr  14085  ivthinclemur  14087  bj-indint  14653  bj-inf2vnlem2  14693  peano4nninf  14725