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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  an3  595  pm5.62dc  958  3simpa  1025  xoror  1428  anxordi  1449  sbidm  1904  reurex  2771  eqimss  3302  eldifi  3351  elinel1  3415  inss1  3451  sopo  4460  wefr  4505  ordtr  4525  opelxp1  4810  relop  4932  ssrelrn  4974  funmo  5395  funrel  5397  funinsn  5433  fnfun  5481  ffn  5536  f1f  5601  f1of1  5641  f1ofo  5649  isof1o  6016  eqopi  6410  1st2nd2  6413  reldmtpos  6528  swoer  6839  ecopover  6911  ecopoverg  6914  fnfi  7255  casef  7435  nninff  7469  lpowlpo  7515  papirr  7618  tapap  7623  dfplpq2  7728  enq0ref  7807  cauappcvgprlemopl  8020  cauappcvgprlemdisj  8025  caucvgprlemopl  8043  caucvgprlemdisj  8048  caucvgprprlemopl  8071  caucvgprprlemopu  8073  caucvgprprlemdisj  8076  peano1nnnn  8226  axrnegex  8253  ltxrlt  8398  1nn  9325  zre  9660  nnssz  9673  ixxss1  10324  ixxss2  10325  ixxss12  10326  iccss2  10364  rge0ssre  10397  elfzuz  10442  uzdisj  10518  nn0disj  10563  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  0wrd0  11353  modfsummodlemstep  12250  mertenslem2  12329  prmnn  12914  prmuz2  12936  nnmaxpw  12979  sqpweven  12981  2sqpwodd  12982  phimullem  13033  hashgcdlem  13046  1arith  13176  ballotfilem2  13287  ctinfom  13378  ctinf  13380  sgrpmgm  13782  mndsgrp  13794  grpmnd  13872  nsgsubg  14068  ghmgrp1  14108  ghmgrp2  14109  ablgrp  14183  cmnmnd  14195  crngring  14420  rimrhm  14588  subrgring  14642  subrgrcl  14644  rhmpropd  14672  domnnzr  14689  drnglring  14717  flddrngd  14725  2idlelbas  14963  rng2idlsubgsubrng  14967  2idlcpblrng  14970  2idlcpbl  14971  qusrhm  14975  assalmod  15116  assaring  15117  psr1clfi  15203  topontop  15252  tpstop  15273  cntop1  15439  cntop2  15440  hmeocn  15543  isxmet2d  15586  metxmet  15593  xmstps  15695  msxms  15696  xmsxmet  15698  msmet  15699  bdxmet  15739  ivthinclemlr  15875  ivthinclemur  15877  mpodvdsmulf1o  16296  uhgr0vb  16542  trliswlk  16844  eupthfi  16909  eupthistrl  16912  bj-indint  17174  bj-inf2vnlem2  17214  peano4nninf  17267  als-no-surprise  17366