Theorem biimpar 297

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 158	. 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:  exbiri  382  bitr  472  eqtr  2195  opabss  4068  euotd  4255  wetriext  4577  sosng  4700  xpsspw  4739  brcogw  4797  funimaexglem  5300  funfni  5317  fnco  5325  fnssres  5330  fn0  5336  fnimadisj  5337  fnimaeq0  5338  foco  5449  foimacnv  5480  fvelimab  5573  fvopab3ig  5591  dff3im  5662  dffo4  5665  fmptco  5683  f1eqcocnv  5792  f1ocnv2d  6075  fnexALT  6112  xp1st  6166  xp2nd  6167  tfrlemiubacc  6331  tfri2d  6337  tfr1onlemubacc  6347  tfrcllemubacc  6360  tfri3  6368  ecelqsg  6588  elqsn0m  6603  fidifsnen  6870  recclnq  7391  nq0a0  7456  qreccl  9642  difelfzle  10134  exfzdc  10240  modifeq2int  10386  frec2uzlt2d  10404  1elfz0hash  10786  caucvgrelemcau  10989  recvalap  11106  fzomaxdiflem  11121  2zsupmax  11234  2zinfmin  11251  fsumparts  11478  ntrivcvgap  11556  divconjdvds  11855  ndvdssub  11935  zsupcllemstep  11946  rplpwr  12028  dvdssqlem  12031  eucalgcvga  12058  mulgcddvds  12094  isprm2lem  12116  powm2modprm  12252  coprimeprodsq  12257  pythagtriplem11  12274  pythagtriplem13  12276  grpidd  12802  ismndd  12838  mulgaddcom  13007  isringd  13220  01eq0ring  13330  uniopn  13504  ntrval  13613  clsval  13614  neival  13646  restdis  13687  lmbrf  13718  cnpnei  13722  dviaddf  14172  dvimulf  14173  logbgt0b  14387  lgslem4  14407  lgsmod  14430  lgsdir2lem2  14433  lgsdir2  14437  lgsne0  14442  lgsmulsqcoprm  14450  lgseisenlem1  14453  2sqlem4  14468