Theorem simplbi 269

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 119	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 111	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.62dc  892  3simpa  941  xoror  1316  anxordi  1337  sbidm  1780  reurex  2581  eqimss  3079  eldifi  3123  elinel1  3187  inss1  3221  sopo  4149  wefr  4194  ordtr  4214  opelxp1  4485  relop  4599  funmo  5043  funrel  5045  funinsn  5076  fnfun  5124  ffn  5174  f1f  5229  f1of1  5265  f1ofo  5273  isof1o  5600  eqopi  5956  1st2nd2  5959  reldmtpos  6032  swoer  6334  ecopover  6404  ecopoverg  6407  fnfi  6700  casef  6833  dfplpq2  6974  enq0ref  7053  cauappcvgprlemopl  7266  cauappcvgprlemdisj  7271  caucvgprlemopl  7289  caucvgprlemdisj  7294  caucvgprprlemopl  7317  caucvgprprlemopu  7319  caucvgprprlemdisj  7322  peano1nnnn  7450  axrnegex  7475  ltxrlt  7613  1nn  8494  zre  8815  nnssz  8828  ixxss1  9383  ixxss2  9384  ixxss12  9385  iccss2  9423  rge0ssre  9456  elfzuz  9497  uzdisj  9568  nn0disj  9610  frecuzrdgtcl  9880  frecuzrdgfunlem  9887  modfsummodlemstep  10912  mertenslem2  10991  prmnn  11431  prmuz2  11451  oddpwdc  11491  sqpweven  11492  2sqpwodd  11493  phimullem  11540  hashgcdlem  11542  topontop  11774  tpstop  11794  bj-indint  12099  bj-inf2vnlem2  12139  nninff  12166  peano4nninf  12168