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  6415  cauappcvgprlemopl  6617  cauappcvgprlemdisj  6622  axrnegex  6743  ltxrlt  6862  1nn  7686  zre  8005  nnssz  8018  ixxss1  8523  ixxss2  8524  ixxss12  8525  iccss2  8563  rge0ssre  8596  elfzuz  8636  uzdisj  8705  nn0disj  8745  frecuzrdgfn  8859  bj-indint  9366  bj-inf2vnlem2  9401