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  614  eqtr  2214  opabss  4098  euotd  4288  wetriext  4614  sosng  4737  xpsspw  4776  brcogw  4836  funimaexglem  5342  funfni  5361  fnco  5369  fnssres  5374  fn0  5380  fnimadisj  5381  fnimaeq0  5382  foco  5494  foimacnv  5525  fvelimab  5620  fvopab3ig  5638  dff3im  5710  dffo4  5713  fmptco  5731  f1eqcocnv  5841  f1ocnv2d  6131  fnexALT  6177  xp1st  6232  xp2nd  6233  tfrlemiubacc  6397  tfri2d  6403  tfr1onlemubacc  6413  tfrcllemubacc  6426  tfri3  6434  ecelqsg  6656  elqsn0m  6671  fidifsnen  6940  recclnq  7476  nq0a0  7541  qreccl  9733  difelfzle  10226  exfzdc  10333  zsupcllemstep  10336  modifeq2int  10495  frec2uzlt2d  10513  zzlesq  10817  1elfz0hash  10915  lennncl  10972  wrdsymb0  10984  caucvgrelemcau  11162  recvalap  11279  fzomaxdiflem  11294  2zsupmax  11408  2zinfmin  11425  fsumparts  11652  ntrivcvgap  11730  fsumdvds  12024  divconjdvds  12031  ndvdssub  12112  rplpwr  12219  dvdssqlem  12222  eucalgcvga  12251  mulgcddvds  12287  isprm2lem  12309  powm2modprm  12446  coprimeprodsq  12451  pythagtriplem11  12468  pythagtriplem13  12470  pcadd2  12535  4sqlem11  12595  grpidd  13085  ismndd  13139  gsumfzz  13197  gsumwmhm  13200  mulgaddcom  13352  resghm  13466  conjnsg  13487  isrngd  13585  isringd  13673  01eq0ring  13821  lspsneq0b  14059  lmodindp1  14060  znf1o  14283  psrgrp  14313  uniopn  14321  ntrval  14430  clsval  14431  neival  14463  restdis  14504  lmbrf  14535  cnpnei  14539  dviaddf  15025  dvimulf  15026  logbgt0b  15286  perfectlem2  15320  lgslem4  15328  lgsmod  15351  lgsdir2lem2  15354  lgsdir2  15358  lgsne0  15363  lgsmulsqcoprm  15371  lgseisenlem1  15395  2lgsoddprm  15438  2sqlem4  15443