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  965  elrab3t  2981  difprsnss  3851  elpw2g  4290  elon2  4519  ideqg  4929  elrnmpt1s  5030  elrnmptg  5032  fun11iun  5658  eqfnfv2  5801  fmpt  5852  elunirn  5966  spc2ed  6463  tposfo2  6532  tposf12  6534  dom2lem  7052  enfii  7170  ac6sfi  7196  ltexprlemm  7961  elreal2  8191  fihasheqf1oi  11209  fprod2dlemstep  12372  bastop2  15168  2lgsoddprm  16215