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:  an3  589  pm5.62dc  951  3simpa  1018  xoror  1421  anxordi  1442  sbidm  1897  reurex  2750  eqimss  3279  eldifi  3327  elinel1  3391  inss1  3425  sopo  4408  wefr  4453  ordtr  4473  opelxp1  4757  relop  4878  ssrelrn  4920  funmo  5339  funrel  5341  funinsn  5376  fnfun  5424  ffn  5479  f1f  5539  f1of1  5579  f1ofo  5587  isof1o  5943  eqopi  6330  1st2nd2  6333  reldmtpos  6414  swoer  6725  ecopover  6797  ecopoverg  6800  fnfi  7129  casef  7281  nninff  7315  lpowlpo  7361  dfplpq2  7567  enq0ref  7646  cauappcvgprlemopl  7859  cauappcvgprlemdisj  7864  caucvgprlemopl  7882  caucvgprlemdisj  7887  caucvgprprlemopl  7910  caucvgprprlemopu  7912  caucvgprprlemdisj  7915  peano1nnnn  8065  axrnegex  8092  ltxrlt  8238  1nn  9147  zre  9476  nnssz  9489  ixxss1  10132  ixxss2  10133  ixxss12  10134  iccss2  10172  rge0ssre  10205  elfzuz  10249  uzdisj  10321  nn0disj  10366  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  0wrd0  11132  modfsummodlemstep  12011  mertenslem2  12090  prmnn  12675  prmuz2  12696  oddpwdc  12739  sqpweven  12740  2sqpwodd  12741  phimullem  12790  hashgcdlem  12803  1arith  12933  ctinfom  13042  ctinf  13044  sgrpmgm  13483  mndsgrp  13497  grpmnd  13583  nsgsubg  13785  ghmgrp1  13825  ghmgrp2  13826  ablgrp  13869  cmnmnd  13881  crngring  14014  rimrhm  14178  subrgring  14231  subrgrcl  14233  rhmpropd  14261  domnnzr  14277  2idlelbas  14523  rng2idlsubgsubrng  14527  2idlcpblrng  14530  2idlcpbl  14531  qusrhm  14535  psr1clfi  14695  topontop  14731  tpstop  14752  cntop1  14918  cntop2  14919  hmeocn  15022  isxmet2d  15065  metxmet  15072  xmstps  15174  msxms  15175  xmsxmet  15177  msmet  15178  bdxmet  15218  ivthinclemlr  15354  ivthinclemur  15356  mpodvdsmulf1o  15707  uhgr0vb  15928  trliswlk  16195  eupthfi  16260  eupthistrl  16263  bj-indint  16476  bj-inf2vnlem2  16516  peano4nninf  16558