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  958  elrab3t  2958  difprsnss  3806  elpw2g  4240  elon2  4467  ideqg  4873  elrnmpt1s  4974  elrnmptg  4976  fun11iun  5595  eqfnfv2  5735  fmpt  5787  elunirn  5896  spc2ed  6385  tposfo2  6419  tposf12  6421  dom2lem  6931  enfii  7044  ac6sfi  7068  ltexprlemm  7795  elreal2  8025  fihasheqf1oi  11017  fprod2dlemstep  12141  bastop2  14766  2lgsoddprm  15800