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  3806  elpw2g  4241  elon2  4468  ideqg  4876  elrnmpt1s  4977  elrnmptg  4979  fun11iun  5598  eqfnfv2  5738  fmpt  5790  elunirn  5899  spc2ed  6390  tposfo2  6424  tposf12  6426  dom2lem  6936  enfii  7049  ac6sfi  7073  ltexprlemm  7803  elreal2  8033  fihasheqf1oi  11026  fprod2dlemstep  12154  bastop2  14779  2lgsoddprm  15813