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  961  elrab3t  2962  difprsnss  3816  elpw2g  4251  elon2  4479  ideqg  4887  elrnmpt1s  4988  elrnmptg  4990  fun11iun  5613  eqfnfv2  5754  fmpt  5805  elunirn  5917  spc2ed  6407  tposfo2  6476  tposf12  6478  dom2lem  6988  enfii  7104  ac6sfi  7130  ltexprlemm  7863  elreal2  8093  fihasheqf1oi  11093  fprod2dlemstep  12244  bastop2  14875  2lgsoddprm  15912