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  eqtr  2195  opabss  4069  euotd  4256  wetriext  4578  sosng  4701  xpsspw  4740  brcogw  4798  funimaexglem  5301  funfni  5318  fnco  5326  fnssres  5331  fn0  5337  fnimadisj  5338  fnimaeq0  5339  foco  5450  foimacnv  5481  fvelimab  5574  fvopab3ig  5592  dff3im  5663  dffo4  5666  fmptco  5684  f1eqcocnv  5794  f1ocnv2d  6077  fnexALT  6114  xp1st  6168  xp2nd  6169  tfrlemiubacc  6333  tfri2d  6339  tfr1onlemubacc  6349  tfrcllemubacc  6362  tfri3  6370  ecelqsg  6590  elqsn0m  6605  fidifsnen  6872  recclnq  7393  nq0a0  7458  qreccl  9644  difelfzle  10136  exfzdc  10242  modifeq2int  10388  frec2uzlt2d  10406  1elfz0hash  10788  caucvgrelemcau  10991  recvalap  11108  fzomaxdiflem  11123  2zsupmax  11236  2zinfmin  11253  fsumparts  11480  ntrivcvgap  11558  divconjdvds  11857  ndvdssub  11937  zsupcllemstep  11948  rplpwr  12030  dvdssqlem  12033  eucalgcvga  12060  mulgcddvds  12096  isprm2lem  12118  powm2modprm  12254  coprimeprodsq  12259  pythagtriplem11  12276  pythagtriplem13  12278  grpidd  12807  ismndd  12843  mulgaddcom  13012  isringd  13225  01eq0ring  13335  uniopn  13540  ntrval  13649  clsval  13650  neival  13682  restdis  13723  lmbrf  13754  cnpnei  13758  dviaddf  14208  dvimulf  14209  logbgt0b  14423  lgslem4  14443  lgsmod  14466  lgsdir2lem2  14469  lgsdir2  14473  lgsne0  14478  lgsmulsqcoprm  14486  lgseisenlem1  14489  2sqlem4  14504