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  618  eqtr  2249  opabss  4153  euotd  4347  wetriext  4675  sosng  4799  xpsspw  4838  brcogw  4899  funimaexglem  5413  funfni  5432  fnco  5440  fnssres  5445  fn0  5452  fnimadisj  5453  fnimaeq0  5454  foco  5570  foimacnv  5601  fvelimab  5702  fvopab3ig  5720  dff3im  5792  dffo4  5795  fmptco  5813  f1eqcocnv  5931  f1ocnv2d  6226  fnexALT  6272  xp1st  6327  xp2nd  6328  tfrlemiubacc  6495  tfri2d  6501  tfr1onlemubacc  6511  tfrcllemubacc  6524  tfri3  6532  ecelqsg  6756  elqsn0m  6771  fidifsnen  7056  pr1or2  7398  recclnq  7611  nq0a0  7676  qreccl  9875  difelfzle  10368  exfzdc  10485  zsupcllemstep  10488  modifeq2int  10647  frec2uzlt2d  10665  zzlesq  10969  fihashgt0  11068  1elfz0hash  11069  lennncl  11132  wrdsymb0  11145  ccatsymb  11178  ccatlid  11182  ccatass  11184  ccatswrd  11250  swrdccat2  11251  ccatpfx  11281  swrdccatfn  11304  swrdccat  11315  caucvgrelemcau  11540  recvalap  11657  fzomaxdiflem  11672  2zsupmax  11786  2zinfmin  11803  fsumparts  12030  ntrivcvgap  12108  fsumdvds  12402  divconjdvds  12409  ndvdssub  12490  rplpwr  12597  dvdssqlem  12600  eucalgcvga  12629  mulgcddvds  12665  isprm2lem  12687  powm2modprm  12824  coprimeprodsq  12829  pythagtriplem11  12846  pythagtriplem13  12848  pcadd2  12913  4sqlem11  12973  grpidd  13465  ismndd  13519  gsumfzz  13577  gsumwmhm  13580  mulgaddcom  13732  resghm  13846  conjnsg  13867  isrngd  13965  isringd  14053  01eq0ring  14202  lspsneq0b  14440  lmodindp1  14441  znf1o  14664  psrgrp  14698  uniopn  14724  ntrval  14833  clsval  14834  neival  14866  restdis  14907  lmbrf  14938  cnpnei  14942  dviaddf  15428  dvimulf  15429  logbgt0b  15689  perfectlem2  15723  lgslem4  15731  lgsmod  15754  lgsdir2lem2  15757  lgsdir2  15761  lgsne0  15766  lgsmulsqcoprm  15774  lgseisenlem1  15798  2lgsoddprm  15841  2sqlem4  15846  wlk1walkdom  16209  wlkreslem  16228