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  2211  opabss  4094  euotd  4284  wetriext  4610  sosng  4733  xpsspw  4772  brcogw  4832  funimaexglem  5338  funfni  5355  fnco  5363  fnssres  5368  fn0  5374  fnimadisj  5375  fnimaeq0  5376  foco  5488  foimacnv  5519  fvelimab  5614  fvopab3ig  5632  dff3im  5704  dffo4  5707  fmptco  5725  f1eqcocnv  5835  f1ocnv2d  6124  fnexALT  6165  xp1st  6220  xp2nd  6221  tfrlemiubacc  6385  tfri2d  6391  tfr1onlemubacc  6401  tfrcllemubacc  6414  tfri3  6422  ecelqsg  6644  elqsn0m  6659  fidifsnen  6928  recclnq  7454  nq0a0  7519  qreccl  9710  difelfzle  10203  exfzdc  10310  modifeq2int  10460  frec2uzlt2d  10478  zzlesq  10782  1elfz0hash  10880  lennncl  10937  wrdsymb0  10949  caucvgrelemcau  11127  recvalap  11244  fzomaxdiflem  11259  2zsupmax  11372  2zinfmin  11389  fsumparts  11616  ntrivcvgap  11694  divconjdvds  11994  ndvdssub  12074  zsupcllemstep  12085  rplpwr  12167  dvdssqlem  12170  eucalgcvga  12199  mulgcddvds  12235  isprm2lem  12257  powm2modprm  12393  coprimeprodsq  12398  pythagtriplem11  12415  pythagtriplem13  12417  pcadd2  12482  4sqlem11  12542  grpidd  12969  ismndd  13021  gsumfzz  13070  gsumwmhm  13073  mulgaddcom  13219  resghm  13333  conjnsg  13354  isrngd  13452  isringd  13540  01eq0ring  13688  lspsneq0b  13926  lmodindp1  13927  znf1o  14150  uniopn  14180  ntrval  14289  clsval  14290  neival  14322  restdis  14363  lmbrf  14394  cnpnei  14398  dviaddf  14884  dvimulf  14885  logbgt0b  15139  lgslem4  15160  lgsmod  15183  lgsdir2lem2  15186  lgsdir2  15190  lgsne0  15195  lgsmulsqcoprm  15203  lgseisenlem1  15227  2lgsoddprm  15270  2sqlem4  15275