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  961  elrab3t  2971  difprsnss  3831  elpw2g  4267  elon2  4496  ideqg  4905  elrnmpt1s  5006  elrnmptg  5008  fun11iun  5634  eqfnfv2  5775  fmpt  5826  elunirn  5938  spc2ed  6428  tposfo2  6497  tposf12  6499  dom2lem  7010  enfii  7128  ac6sfi  7154  ltexprlemm  7914  elreal2  8144  fihasheqf1oi  11148  fprod2dlemstep  12304  bastop2  14941  2lgsoddprm  15978