Theorem biimpar 295

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpar	⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Proof of Theorem biimpar

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprd 157	. 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:  exbiri  379  bitr  463  eqtr  2157  opabss  3992  euotd  4176  wetriext  4491  sosng  4612  xpsspw  4651  brcogw  4708  funimaexglem  5206  funfni  5223  fnco  5231  fnssres  5236  fn0  5242  fnimadisj  5243  fnimaeq0  5244  foco  5355  foimacnv  5385  fvelimab  5477  fvopab3ig  5495  dff3im  5565  dffo4  5568  fmptco  5586  f1eqcocnv  5692  f1ocnv2d  5974  fnexALT  6011  xp1st  6063  xp2nd  6064  tfrlemiubacc  6227  tfri2d  6233  tfr1onlemubacc  6243  tfrcllemubacc  6256  tfri3  6264  ecelqsg  6482  elqsn0m  6497  fidifsnen  6764  recclnq  7207  nq0a0  7272  qreccl  9441  difelfzle  9918  exfzdc  10024  modifeq2int  10166  frec2uzlt2d  10184  1elfz0hash  10559  caucvgrelemcau  10759  recvalap  10876  fzomaxdiflem  10891  2zsupmax  11004  fsumparts  11246  ntrivcvgap  11324  divconjdvds  11554  ndvdssub  11634  zsupcllemstep  11645  rplpwr  11722  dvdssqlem  11725  eucalgcvga  11746  mulgcddvds  11782  isprm2lem  11804  uniopn  12178  ntrval  12289  clsval  12290  neival  12322  restdis  12363  lmbrf  12394  cnpnei  12398  dviaddf  12848  dvimulf  12849