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  2919  difprsnss  3760  elpw2g  4189  elon2  4411  ideqg  4817  elrnmpt1s  4916  elrnmptg  4918  fun11iun  5525  eqfnfv2  5660  fmpt  5712  elunirn  5813  spc2ed  6291  tposfo2  6325  tposf12  6327  dom2lem  6831  enfii  6935  ac6sfi  6959  ltexprlemm  7667  elreal2  7897  fihasheqf1oi  10879  fprod2dlemstep  11787  bastop2  14320  2lgsoddprm  15354