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 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  exbiri  382  bitr  476  biadanid  622  eqtr  2256  opabss  4196  euotd  4397  wetriext  4726  sosng  4850  xpsspw  4889  brcogw  4951  funimaexglem  5467  funfni  5486  fnco  5494  fnssres  5499  fn0  5506  fnimadisj  5507  fnimaeq0  5508  foco  5629  foimacnv  5660  fvelimab  5762  fvopab3ig  5782  dff3im  5856  dffo4  5859  fmptco  5877  f1eqcocnv  6000  f1ocnv2d  6297  f1o3d  6301  fnexALT  6344  elabreximd  6360  xp1st  6403  xp2nd  6404  tfrlemiubacc  6605  tfri2d  6611  tfr1onlemubacc  6621  tfrcllemubacc  6634  tfri3  6642  ecelqsg  6866  elqsn0m  6881  fidifsnen  7176  pr1or2  7546  recclnq  7765  nq0a0  7830  qreccl  10058  difelfzle  10558  exfzdc  10676  zsupcllemstep  10679  modifeq2int  10844  frec2uzlt2d  10862  zzlesq  11167  fihashgt0  11268  1elfz0hash  11269  lennncl  11346  wrdsymb0  11359  ccatsymb  11392  ccatlid  11396  ccatass  11398  ccatswrd  11464  swrdccat2  11465  ccatpfx  11495  swrdccatfn  11518  swrdccat  11529  caucvgrelemcau  11768  recvalap  11886  fzomaxdiflem  11901  2zsupmax  12015  2zinfmin  12034  fsumparts  12262  ntrivcvgap  12340  fsumdvds  12634  divconjdvds  12641  ndvdssub  12722  rplpwr  12829  dvdssqlem  12832  eucalgcvga  12861  mulgcddvds  12897  isprm2lem  12919  powm2modprm  13060  coprimeprodsq  13065  pythagtriplem11  13082  pythagtriplem13  13084  pcadd2  13149  4sqlem11  13209  grpidd  13762  ismndd  13809  gzsumwmhm  13862  mulgaddcom  14008  resghm  14122  conjnsg  14143  isrngd  14359  isringd  14453  01eq0ring  14605  lspsneq0b  14873  lmodindp1  14874  znf1o  15095  aspval  15124  psrgrp  15195  uniopn  15227  ntrval  15336  clsval  15337  neival  15369  restdis  15410  lmbrf  15441  cnpnei  15445  dviaddf  15931  dvimulf  15932  logbgt0b  16202  pellexlem2  16230  perfectlem2  16300  bposlem3  16313  lgslem4  16327  lgsmod  16350  lgsdir2lem2  16353  lgsdir2  16357  lgsne0  16362  lgsmulsqcoprm  16370  lgseisenlem1  16394  2lgsoddprm  16437  2sqlem4  16442  wlk1walkdom  16805  wlkreslem  16824