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  954  elrab3t  2916  difprsnss  3757  elpw2g  4186  elon2  4408  ideqg  4814  elrnmpt1s  4913  elrnmptg  4915  fun11iun  5522  eqfnfv2  5657  fmpt  5709  elunirn  5810  spc2ed  6288  tposfo2  6322  tposf12  6324  dom2lem  6828  enfii  6932  ac6sfi  6956  ltexprlemm  7662  elreal2  7892  fihasheqf1oi  10861  fprod2dlemstep  11768  bastop2  14263  2lgsoddprm  15270