Theorem biimparc 297

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 159	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	imp 123	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biantr  947  elrab3t  2885  difprsnss  3716  elpw2g  4140  elon2  4359  ideqg  4760  elrnmpt1s  4859  elrnmptg  4861  fun11iun  5461  eqfnfv2  5592  fmpt  5644  elunirn  5743  spc2ed  6210  tposfo2  6244  tposf12  6246  dom2lem  6747  enfii  6849  ac6sfi  6873  ltexprlemm  7551  elreal2  7781  fihasheqf1oi  10711  fprod2dlemstep  11574  bastop2  12839