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  476  biadanid  622  eqtr  2256  opabss  4190  euotd  4390  wetriext  4719  sosng  4843  xpsspw  4882  brcogw  4944  funimaexglem  5459  funfni  5478  fnco  5486  fnssres  5491  fn0  5498  fnimadisj  5499  fnimaeq0  5500  foco  5621  foimacnv  5652  fvelimab  5753  fvopab3ig  5773  dff3im  5844  dffo4  5847  fmptco  5865  f1eqcocnv  5987  f1ocnv2d  6284  f1o3d  6288  fnexALT  6330  elabreximd  6346  xp1st  6389  xp2nd  6390  tfrlemiubacc  6591  tfri2d  6597  tfr1onlemubacc  6607  tfrcllemubacc  6620  tfri3  6628  ecelqsg  6852  elqsn0m  6867  fidifsnen  7162  pr1or2  7530  recclnq  7749  nq0a0  7814  qreccl  10021  difelfzle  10519  exfzdc  10637  zsupcllemstep  10640  modifeq2int  10801  frec2uzlt2d  10819  zzlesq  11124  fihashgt0  11224  1elfz0hash  11225  lennncl  11302  wrdsymb0  11315  ccatsymb  11348  ccatlid  11352  ccatass  11354  ccatswrd  11420  swrdccat2  11421  ccatpfx  11451  swrdccatfn  11474  swrdccat  11485  caucvgrelemcau  11724  recvalap  11841  fzomaxdiflem  11856  2zsupmax  11970  2zinfmin  11987  fsumparts  12215  ntrivcvgap  12293  fsumdvds  12587  divconjdvds  12594  ndvdssub  12675  rplpwr  12782  dvdssqlem  12785  eucalgcvga  12814  mulgcddvds  12850  isprm2lem  12872  powm2modprm  13009  coprimeprodsq  13014  pythagtriplem11  13031  pythagtriplem13  13033  pcadd2  13098  4sqlem11  13158  grpidd  13680  ismndd  13727  gzsumwmhm  13780  mulgaddcom  13926  resghm  14040  conjnsg  14061  isrngd  14227  isringd  14319  01eq0ring  14469  lspsneq0b  14736  lmodindp1  14737  znf1o  14958  psrgrp  14999  uniopn  15025  ntrval  15134  clsval  15135  neival  15167  restdis  15208  lmbrf  15239  cnpnei  15243  dviaddf  15729  dvimulf  15730  logbgt0b  15991  pellexlem2  16006  perfectlem2  16028  lgslem4  16036  lgsmod  16059  lgsdir2lem2  16062  lgsdir2  16066  lgsne0  16071  lgsmulsqcoprm  16079  lgseisenlem1  16103  2lgsoddprm  16146  2sqlem4  16151  wlk1walkdom  16514  wlkreslem  16533