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  4148  euotd  4341  wetriext  4669  sosng  4792  xpsspw  4831  brcogw  4891  funimaexglem  5404  funfni  5423  fnco  5431  fnssres  5436  fn0  5443  fnimadisj  5444  fnimaeq0  5445  foco  5561  foimacnv  5592  fvelimab  5692  fvopab3ig  5710  dff3im  5782  dffo4  5785  fmptco  5803  f1eqcocnv  5921  f1ocnv2d  6216  fnexALT  6262  xp1st  6317  xp2nd  6318  tfrlemiubacc  6482  tfri2d  6488  tfr1onlemubacc  6498  tfrcllemubacc  6511  tfri3  6519  ecelqsg  6743  elqsn0m  6758  fidifsnen  7040  pr1or2  7378  recclnq  7590  nq0a0  7655  qreccl  9849  difelfzle  10342  exfzdc  10458  zsupcllemstep  10461  modifeq2int  10620  frec2uzlt2d  10638  zzlesq  10942  fihashgt0  11040  1elfz0hash  11041  lennncl  11104  wrdsymb0  11117  ccatsymb  11150  ccatlid  11154  ccatass  11156  ccatswrd  11217  swrdccat2  11218  ccatpfx  11248  swrdccatfn  11271  swrdccat  11282  caucvgrelemcau  11506  recvalap  11623  fzomaxdiflem  11638  2zsupmax  11752  2zinfmin  11769  fsumparts  11996  ntrivcvgap  12074  fsumdvds  12368  divconjdvds  12375  ndvdssub  12456  rplpwr  12563  dvdssqlem  12566  eucalgcvga  12595  mulgcddvds  12631  isprm2lem  12653  powm2modprm  12790  coprimeprodsq  12795  pythagtriplem11  12812  pythagtriplem13  12814  pcadd2  12879  4sqlem11  12939  grpidd  13431  ismndd  13485  gsumfzz  13543  gsumwmhm  13546  mulgaddcom  13698  resghm  13812  conjnsg  13833  isrngd  13931  isringd  14019  01eq0ring  14168  lspsneq0b  14406  lmodindp1  14407  znf1o  14630  psrgrp  14664  uniopn  14690  ntrval  14799  clsval  14800  neival  14832  restdis  14873  lmbrf  14904  cnpnei  14908  dviaddf  15394  dvimulf  15395  logbgt0b  15655  perfectlem2  15689  lgslem4  15697  lgsmod  15720  lgsdir2lem2  15723  lgsdir2  15727  lgsne0  15732  lgsmulsqcoprm  15740  lgseisenlem1  15764  2lgsoddprm  15807  2sqlem4  15812  wlk1walkdom  16100  wlkreslem  16117