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  7478  nq0a0  7543  qreccl  9735  difelfzle  10228  exfzdc  10335  zsupcllemstep  10338  modifeq2int  10497  frec2uzlt2d  10515  zzlesq  10819  1elfz0hash  10917  lennncl  10974  wrdsymb0  10986  caucvgrelemcau  11164  recvalap  11281  fzomaxdiflem  11296  2zsupmax  11410  2zinfmin  11427  fsumparts  11654  ntrivcvgap  11732  fsumdvds  12026  divconjdvds  12033  ndvdssub  12114  rplpwr  12221  dvdssqlem  12224  eucalgcvga  12253  mulgcddvds  12289  isprm2lem  12311  powm2modprm  12448  coprimeprodsq  12453  pythagtriplem11  12470  pythagtriplem13  12472  pcadd2  12537  4sqlem11  12597  grpidd  13087  ismndd  13141  gsumfzz  13199  gsumwmhm  13202  mulgaddcom  13354  resghm  13468  conjnsg  13489  isrngd  13587  isringd  13675  01eq0ring  13823  lspsneq0b  14061  lmodindp1  14062  znf1o  14285  psrgrp  14319  uniopn  14345  ntrval  14454  clsval  14455  neival  14487  restdis  14528  lmbrf  14559  cnpnei  14563  dviaddf  15049  dvimulf  15050  logbgt0b  15310  perfectlem2  15344  lgslem4  15352  lgsmod  15375  lgsdir2lem2  15378  lgsdir2  15382  lgsne0  15387  lgsmulsqcoprm  15395  lgseisenlem1  15419  2lgsoddprm  15462  2sqlem4  15467