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  954  elrab3t  2915  difprsnss  3756  elpw2g  4185  elon2  4407  ideqg  4813  elrnmpt1s  4912  elrnmptg  4914  fun11iun  5521  eqfnfv2  5656  fmpt  5708  elunirn  5809  spc2ed  6286  tposfo2  6320  tposf12  6322  dom2lem  6826  enfii  6930  ac6sfi  6954  ltexprlemm  7660  elreal2  7890  fihasheqf1oi  10858  fprod2dlemstep  11765  bastop2  14252