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  936  elrab3t  2834  difprsnss  3653  elpw2g  4076  elon2  4293  ideqg  4685  elrnmpt1s  4784  elrnmptg  4786  fun11iun  5381  eqfnfv2  5512  fmpt  5563  elunirn  5660  spc2ed  6123  tposfo2  6157  tposf12  6159  dom2lem  6659  enfii  6761  ac6sfi  6785  ltexprlemm  7401  elreal2  7631  fihasheqf1oi  10527  bastop2  12242