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  2959  difprsnss  3809  elpw2g  4244  elon2  4471  ideqg  4879  elrnmpt1s  4980  elrnmptg  4982  fun11iun  5601  eqfnfv2  5741  fmpt  5793  elunirn  5902  spc2ed  6393  tposfo2  6428  tposf12  6430  dom2lem  6940  enfii  7056  ac6sfi  7082  ltexprlemm  7813  elreal2  8043  fihasheqf1oi  11042  fprod2dlemstep  12176  bastop2  14801  2lgsoddprm  15835