Theorem biimparc 297

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 159	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	imp 123	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biantr  942  elrab3t  2881  difprsnss  3711  elpw2g  4135  elon2  4354  ideqg  4755  elrnmpt1s  4854  elrnmptg  4856  fun11iun  5453  eqfnfv2  5584  fmpt  5635  elunirn  5734  spc2ed  6201  tposfo2  6235  tposf12  6237  dom2lem  6738  enfii  6840  ac6sfi  6864  ltexprlemm  7541  elreal2  7771  fihasheqf1oi  10701  fprod2dlemstep  11563  bastop2  12724