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  biadanid  616  eqtr  2247  opabss  4151  euotd  4345  wetriext  4673  sosng  4797  xpsspw  4836  brcogw  4897  funimaexglem  5410  funfni  5429  fnco  5437  fnssres  5442  fn0  5449  fnimadisj  5450  fnimaeq0  5451  foco  5567  foimacnv  5598  fvelimab  5698  fvopab3ig  5716  dff3im  5788  dffo4  5791  fmptco  5809  f1eqcocnv  5927  f1ocnv2d  6222  fnexALT  6268  xp1st  6323  xp2nd  6324  tfrlemiubacc  6491  tfri2d  6497  tfr1onlemubacc  6507  tfrcllemubacc  6520  tfri3  6528  ecelqsg  6752  elqsn0m  6767  fidifsnen  7052  pr1or2  7390  recclnq  7602  nq0a0  7667  qreccl  9866  difelfzle  10359  exfzdc  10476  zsupcllemstep  10479  modifeq2int  10638  frec2uzlt2d  10656  zzlesq  10960  fihashgt0  11059  1elfz0hash  11060  lennncl  11123  wrdsymb0  11136  ccatsymb  11169  ccatlid  11173  ccatass  11175  ccatswrd  11241  swrdccat2  11242  ccatpfx  11272  swrdccatfn  11295  swrdccat  11306  caucvgrelemcau  11531  recvalap  11648  fzomaxdiflem  11663  2zsupmax  11777  2zinfmin  11794  fsumparts  12021  ntrivcvgap  12099  fsumdvds  12393  divconjdvds  12400  ndvdssub  12481  rplpwr  12588  dvdssqlem  12591  eucalgcvga  12620  mulgcddvds  12656  isprm2lem  12678  powm2modprm  12815  coprimeprodsq  12820  pythagtriplem11  12837  pythagtriplem13  12839  pcadd2  12904  4sqlem11  12964  grpidd  13456  ismndd  13510  gsumfzz  13568  gsumwmhm  13571  mulgaddcom  13723  resghm  13837  conjnsg  13858  isrngd  13956  isringd  14044  01eq0ring  14193  lspsneq0b  14431  lmodindp1  14432  znf1o  14655  psrgrp  14689  uniopn  14715  ntrval  14824  clsval  14825  neival  14857  restdis  14898  lmbrf  14929  cnpnei  14933  dviaddf  15419  dvimulf  15420  logbgt0b  15680  perfectlem2  15714  lgslem4  15722  lgsmod  15745  lgsdir2lem2  15748  lgsdir2  15752  lgsne0  15757  lgsmulsqcoprm  15765  lgseisenlem1  15789  2lgsoddprm  15832  2sqlem4  15837  wlk1walkdom  16156  wlkreslem  16173