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  2975  difprsnss  3837  elpw2g  4273  elon2  4502  ideqg  4911  elrnmpt1s  5012  elrnmptg  5014  fun11iun  5640  eqfnfv2  5781  fmpt  5832  elunirn  5945  spc2ed  6442  tposfo2  6511  tposf12  6513  dom2lem  7024  enfii  7142  ac6sfi  7168  ltexprlemm  7931  elreal2  8161  fihasheqf1oi  11175  fprod2dlemstep  12333  bastop2  15061  2lgsoddprm  16098