Theorem simplbi 272

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-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.62dc  929  3simpa  978  xoror  1357  anxordi  1378  sbidm  1823  reurex  2642  eqimss  3146  eldifi  3193  elinel1  3257  inss1  3291  sopo  4230  wefr  4275  ordtr  4295  opelxp1  4568  relop  4684  funmo  5133  funrel  5135  funinsn  5167  fnfun  5215  ffn  5267  f1f  5323  f1of1  5359  f1ofo  5367  isof1o  5701  eqopi  6063  1st2nd2  6066  reldmtpos  6143  swoer  6450  ecopover  6520  ecopoverg  6523  fnfi  6818  casef  6966  dfplpq2  7155  enq0ref  7234  cauappcvgprlemopl  7447  cauappcvgprlemdisj  7452  caucvgprlemopl  7470  caucvgprlemdisj  7475  caucvgprprlemopl  7498  caucvgprprlemopu  7500  caucvgprprlemdisj  7503  peano1nnnn  7653  axrnegex  7680  ltxrlt  7823  1nn  8724  zre  9051  nnssz  9064  ixxss1  9680  ixxss2  9681  ixxss12  9682  iccss2  9720  rge0ssre  9753  elfzuz  9795  uzdisj  9866  nn0disj  9908  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  modfsummodlemstep  11219  mertenslem2  11298  prmnn  11780  prmuz2  11800  oddpwdc  11841  sqpweven  11842  2sqpwodd  11843  phimullem  11890  hashgcdlem  11892  ctinfom  11930  ctinf  11932  topontop  12170  tpstop  12191  cntop1  12359  cntop2  12360  hmeocn  12463  isxmet2d  12506  metxmet  12513  xmstps  12615  msxms  12616  xmsxmet  12618  msmet  12619  bdxmet  12659  ivthinclemlr  12773  ivthinclemur  12775  bj-indint  13118  bj-inf2vnlem2  13158  nninff  13187  peano4nninf  13189