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  591  pm5.62dc  954  3simpa  1021  xoror  1424  anxordi  1445  sbidm  1900  reurex  2765  eqimss  3296  eldifi  3345  elinel1  3409  inss1  3445  sopo  4439  wefr  4484  ordtr  4504  opelxp1  4788  relop  4910  ssrelrn  4952  funmo  5372  funrel  5374  funinsn  5410  fnfun  5458  ffn  5513  f1f  5578  f1of1  5618  f1ofo  5626  isof1o  5986  eqopi  6379  1st2nd2  6382  reldmtpos  6497  swoer  6808  ecopover  6880  ecopoverg  6883  fnfi  7216  casef  7392  nninff  7426  lpowlpo  7472  papirr  7575  tapap  7580  dfplpq2  7685  enq0ref  7764  cauappcvgprlemopl  7977  cauappcvgprlemdisj  7982  caucvgprlemopl  8000  caucvgprlemdisj  8005  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemdisj  8033  peano1nnnn  8183  axrnegex  8210  ltxrlt  8355  1nn  9268  zre  9601  nnssz  9614  ixxss1  10259  ixxss2  10260  ixxss12  10261  iccss2  10299  rge0ssre  10332  elfzuz  10377  uzdisj  10452  nn0disj  10497  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  0wrd0  11278  modfsummodlemstep  12171  mertenslem2  12250  prmnn  12835  prmuz2  12856  oddpwdc  12899  sqpweven  12900  2sqpwodd  12901  phimullem  12950  hashgcdlem  12963  1arith  13093  ballotfilem2  13175  ctinfom  13266  ctinf  13268  sgrpmgm  13673  mndsgrp  13685  grpmnd  13765  nsgsubg  13961  ghmgrp1  14001  ghmgrp2  14002  ablgrp  14045  cmnmnd  14057  crngring  14254  rimrhm  14419  subrgring  14473  subrgrcl  14475  rhmpropd  14503  domnnzr  14520  drnglring  14548  flddrngd  14556  2idlelbas  14793  rng2idlsubgsubrng  14797  2idlcpblrng  14800  2idlcpbl  14801  qusrhm  14805  psr1clfi  14972  topontop  15008  tpstop  15029  cntop1  15195  cntop2  15196  hmeocn  15299  isxmet2d  15342  metxmet  15349  xmstps  15451  msxms  15452  xmsxmet  15454  msmet  15455  bdxmet  15495  ivthinclemlr  15631  ivthinclemur  15633  mpodvdsmulf1o  15987  uhgr0vb  16208  trliswlk  16510  eupthfi  16575  eupthistrl  16578  bj-indint  16840  bj-inf2vnlem2  16880  peano4nninf  16923