Theorem biimparc 299

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimparc	⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Proof of Theorem biimparc

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprcd 160	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	imp 124	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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biantr  952  elrab3t  2894  difprsnss  3732  elpw2g  4158  elon2  4378  ideqg  4780  elrnmpt1s  4879  elrnmptg  4881  fun11iun  5484  eqfnfv2  5617  fmpt  5669  elunirn  5770  spc2ed  6237  tposfo2  6271  tposf12  6273  dom2lem  6775  enfii  6877  ac6sfi  6901  ltexprlemm  7602  elreal2  7832  fihasheqf1oi  10770  fprod2dlemstep  11633  bastop2  13724