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  958  elrab3t  2958  difprsnss  3805  elpw2g  4239  elon2  4464  ideqg  4870  elrnmpt1s  4970  elrnmptg  4972  fun11iun  5589  eqfnfv2  5726  fmpt  5778  elunirn  5883  spc2ed  6369  tposfo2  6403  tposf12  6405  dom2lem  6913  enfii  7024  ac6sfi  7048  ltexprlemm  7775  elreal2  8005  fihasheqf1oi  10996  fprod2dlemstep  12119  bastop2  14743  2lgsoddprm  15777