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  3278  eldifi  3326  elinel1  3390  inss1  3424  sopo  4404  wefr  4449  ordtr  4469  opelxp1  4753  relop  4872  ssrelrn  4914  funmo  5333  funrel  5335  funinsn  5370  fnfun  5418  ffn  5473  f1f  5533  f1of1  5573  f1ofo  5581  isof1o  5937  eqopi  6324  1st2nd2  6327  reldmtpos  6405  swoer  6716  ecopover  6788  ecopoverg  6791  fnfi  7111  casef  7263  nninff  7297  lpowlpo  7343  dfplpq2  7549  enq0ref  7628  cauappcvgprlemopl  7841  cauappcvgprlemdisj  7846  caucvgprlemopl  7864  caucvgprlemdisj  7869  caucvgprprlemopl  7892  caucvgprprlemopu  7894  caucvgprprlemdisj  7897  peano1nnnn  8047  axrnegex  8074  ltxrlt  8220  1nn  9129  zre  9458  nnssz  9471  ixxss1  10108  ixxss2  10109  ixxss12  10110  iccss2  10148  rge0ssre  10181  elfzuz  10225  uzdisj  10297  nn0disj  10342  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  0wrd0  11105  modfsummodlemstep  11976  mertenslem2  12055  prmnn  12640  prmuz2  12661  oddpwdc  12704  sqpweven  12705  2sqpwodd  12706  phimullem  12755  hashgcdlem  12768  1arith  12898  ctinfom  13007  ctinf  13009  sgrpmgm  13448  mndsgrp  13462  grpmnd  13548  nsgsubg  13750  ghmgrp1  13790  ghmgrp2  13791  ablgrp  13834  cmnmnd  13846  crngring  13979  rimrhm  14143  subrgring  14196  subrgrcl  14198  rhmpropd  14226  domnnzr  14242  2idlelbas  14488  rng2idlsubgsubrng  14492  2idlcpblrng  14495  2idlcpbl  14496  qusrhm  14500  psr1clfi  14660  topontop  14696  tpstop  14717  cntop1  14883  cntop2  14884  hmeocn  14987  isxmet2d  15030  metxmet  15037  xmstps  15139  msxms  15140  xmsxmet  15142  msmet  15143  bdxmet  15183  ivthinclemlr  15319  ivthinclemur  15321  mpodvdsmulf1o  15672  uhgr0vb  15892  trliswlk  16105  bj-indint  16318  bj-inf2vnlem2  16358  peano4nninf  16402