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  2907  difprsnss  3745  elpw2g  4174  elon2  4394  ideqg  4796  elrnmpt1s  4895  elrnmptg  4897  fun11iun  5501  eqfnfv2  5635  fmpt  5687  elunirn  5788  spc2ed  6259  tposfo2  6293  tposf12  6295  dom2lem  6799  enfii  6903  ac6sfi  6927  ltexprlemm  7630  elreal2  7860  fihasheqf1oi  10802  fprod2dlemstep  11665  bastop2  14061