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  6606  tfri2d  6612  tfr1onlemubacc  6622  tfrcllemubacc  6635  tfri3  6643  ecelqsg  6867  elqsn0m  6882  fidifsnen  7178  pr1or2  7546  recclnq  7765  nq0a0  7830  qreccl  10057  difelfzle  10557  exfzdc  10675  zsupcllemstep  10678  modifeq2int  10843  frec2uzlt2d  10861  zzlesq  11166  fihashgt0  11267  1elfz0hash  11268  lennncl  11345  wrdsymb0  11358  ccatsymb  11391  ccatlid  11395  ccatass  11397  ccatswrd  11463  swrdccat2  11464  ccatpfx  11494  swrdccatfn  11517  swrdccat  11528  caucvgrelemcau  11767  recvalap  11885  fzomaxdiflem  11900  2zsupmax  12014  2zinfmin  12033  fsumparts  12261  ntrivcvgap  12339  fsumdvds  12633  divconjdvds  12640  ndvdssub  12721  rplpwr  12828  dvdssqlem  12831  eucalgcvga  12860  mulgcddvds  12896  isprm2lem  12918  powm2modprm  13059  coprimeprodsq  13064  pythagtriplem11  13081  pythagtriplem13  13083  pcadd2  13148  4sqlem11  13208  grpidd  13761  ismndd  13808  gzsumwmhm  13861  mulgaddcom  14007  resghm  14121  conjnsg  14142  isrngd  14358  isringd  14452  01eq0ring  14604  lspsneq0b  14872  lmodindp1  14873  znf1o  15094  aspval  15123  psrgrp  15204  uniopn  15244  ntrval  15353  clsval  15354  neival  15386  restdis  15427  lmbrf  15458  cnpnei  15462  dviaddf  15948  dvimulf  15949  logbgt0b  16219  pellexlem2  16247  perfectlem2  16317  bposlem3  16330  lgslem4  16344  lgsmod  16367  lgsdir2lem2  16370  lgsdir2  16374  lgsne0  16379  lgsmulsqcoprm  16387  lgseisenlem1  16411  2lgsoddprm  16454  2sqlem4  16459  wlk1walkdom  16822  wlkreslem  16841