Theorem simplbi 259

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 113	. 2 ⊢ (φ → (ψ ∧ χ))
3	2	simpld 105	1 ⊢ (φ → ψ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.62dc  851  3simpa  900  anxordi  1288  sbidm  1728  reurex  2517  eqimss  2991  pssss  3033  eldifi  3060  inss1  3151  sopo  4041  ordtr  4081  opelxp1  4320  relop  4429  funmo  4860  funrel  4862  fnfun  4939  ffn  4989  f1f  5035  f1of1  5068  f1ofo  5076  isof1o  5390  eqopi  5740  1st2nd2  5743  reldmtpos  5809  swoer  6070  ecopover  6140  ecopoverg  6143  dfplpq2  6338  enq0ref  6416  cauappcvgprlemopl  6618  cauappcvgprlemdisj  6623  caucvgprlemopl  6640  caucvgprlemdisj  6645  axrnegex  6763  ltxrlt  6882  1nn  7706  zre  8025  nnssz  8038  ixxss1  8543  ixxss2  8544  ixxss12  8545  iccss2  8583  rge0ssre  8616  elfzuz  8656  uzdisj  8725  nn0disj  8765  frecuzrdgfn  8879  bj-indint  9390  bj-inf2vnlem2  9431