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  955  elrab3t  2929  difprsnss  3773  elpw2g  4204  elon2  4427  ideqg  4833  elrnmpt1s  4933  elrnmptg  4935  fun11iun  5550  eqfnfv2  5685  fmpt  5737  elunirn  5842  spc2ed  6326  tposfo2  6360  tposf12  6362  dom2lem  6870  enfii  6978  ac6sfi  7002  ltexprlemm  7720  elreal2  7950  fihasheqf1oi  10939  fprod2dlemstep  11977  bastop2  14600  2lgsoddprm  15634