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  960  elrab3t  2961  difprsnss  3811  elpw2g  4246  elon2  4473  ideqg  4881  elrnmpt1s  4982  elrnmptg  4984  fun11iun  5604  eqfnfv2  5745  fmpt  5797  elunirn  5907  spc2ed  6398  tposfo2  6433  tposf12  6435  dom2lem  6945  enfii  7061  ac6sfi  7087  ltexprlemm  7820  elreal2  8050  fihasheqf1oi  11050  fprod2dlemstep  12188  bastop2  14814  2lgsoddprm  15848