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 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biantr  965  elrab3t  2981  difprsnss  3853  elpw2g  4294  elon2  4523  ideqg  4933  elrnmpt1s  5034  elrnmptg  5036  fun11iun  5663  eqfnfv2  5810  fmpt  5861  elunirn  5975  spc2ed  6473  tposfo2  6542  tposf12  6544  dom2lem  7063  enfii  7181  ac6sfi  7207  ltexprlemm  7974  elreal2  8204  fihasheqf1oi  11249  fprod2dlemstep  12415  bastop2  15322  2lgsoddprm  16449