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  2691  eqimss  3211  eldifi  3259  elinel1  3323  inss1  3357  sopo  4315  wefr  4360  ordtr  4380  opelxp1  4662  relop  4779  funmo  5233  funrel  5235  funinsn  5267  fnfun  5315  ffn  5367  f1f  5423  f1of1  5462  f1ofo  5470  isof1o  5811  eqopi  6176  1st2nd2  6179  reldmtpos  6257  swoer  6566  ecopover  6636  ecopoverg  6639  fnfi  6939  casef  7090  nninff  7124  lpowlpo  7169  dfplpq2  7356  enq0ref  7435  cauappcvgprlemopl  7648  cauappcvgprlemdisj  7653  caucvgprlemopl  7671  caucvgprlemdisj  7676  caucvgprprlemopl  7699  caucvgprprlemopu  7701  caucvgprprlemdisj  7704  peano1nnnn  7854  axrnegex  7881  ltxrlt  8026  1nn  8933  zre  9260  nnssz  9273  ixxss1  9907  ixxss2  9908  ixxss12  9909  iccss2  9947  rge0ssre  9980  elfzuz  10024  uzdisj  10096  nn0disj  10141  frecuzrdgtcl  10415  frecuzrdgfunlem  10422  modfsummodlemstep  11468  mertenslem2  11547  prmnn  12113  prmuz2  12134  oddpwdc  12177  sqpweven  12178  2sqpwodd  12179  phimullem  12228  hashgcdlem  12241  1arith  12368  ctinfom  12432  ctinf  12434  sgrpmgm  12820  mndsgrp  12830  grpmnd  12892  nsgsubg  13079  ablgrp  13108  cmnmnd  13119  crngring  13229  subrgring  13383  subrgrcl  13385  topontop  13702  tpstop  13723  cntop1  13889  cntop2  13890  hmeocn  13993  isxmet2d  14036  metxmet  14043  xmstps  14145  msxms  14146  xmsxmet  14148  msmet  14149  bdxmet  14189  ivthinclemlr  14303  ivthinclemur  14305  bj-indint  14871  bj-inf2vnlem2  14911  peano4nninf  14944