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  618  eqtr  2249  opabss  4153  euotd  4347  wetriext  4675  sosng  4799  xpsspw  4838  brcogw  4899  funimaexglem  5413  funfni  5432  fnco  5440  fnssres  5445  fn0  5452  fnimadisj  5453  fnimaeq0  5454  foco  5570  foimacnv  5601  fvelimab  5702  fvopab3ig  5720  dff3im  5792  dffo4  5795  fmptco  5813  f1eqcocnv  5932  f1ocnv2d  6227  fnexALT  6273  xp1st  6328  xp2nd  6329  tfrlemiubacc  6496  tfri2d  6502  tfr1onlemubacc  6512  tfrcllemubacc  6525  tfri3  6533  ecelqsg  6757  elqsn0m  6772  fidifsnen  7057  pr1or2  7399  recclnq  7612  nq0a0  7677  qreccl  9876  difelfzle  10369  exfzdc  10487  zsupcllemstep  10490  modifeq2int  10649  frec2uzlt2d  10667  zzlesq  10971  fihashgt0  11070  1elfz0hash  11071  lennncl  11137  wrdsymb0  11150  ccatsymb  11183  ccatlid  11187  ccatass  11189  ccatswrd  11255  swrdccat2  11256  ccatpfx  11286  swrdccatfn  11309  swrdccat  11320  caucvgrelemcau  11558  recvalap  11675  fzomaxdiflem  11690  2zsupmax  11804  2zinfmin  11821  fsumparts  12049  ntrivcvgap  12127  fsumdvds  12421  divconjdvds  12428  ndvdssub  12509  rplpwr  12616  dvdssqlem  12619  eucalgcvga  12648  mulgcddvds  12684  isprm2lem  12706  powm2modprm  12843  coprimeprodsq  12848  pythagtriplem11  12865  pythagtriplem13  12867  pcadd2  12932  4sqlem11  12992  grpidd  13484  ismndd  13538  gsumfzz  13596  gsumwmhm  13599  mulgaddcom  13751  resghm  13865  conjnsg  13886  isrngd  13985  isringd  14073  01eq0ring  14222  lspsneq0b  14460  lmodindp1  14461  znf1o  14684  psrgrp  14718  uniopn  14744  ntrval  14853  clsval  14854  neival  14886  restdis  14927  lmbrf  14958  cnpnei  14962  dviaddf  15448  dvimulf  15449  logbgt0b  15709  perfectlem2  15743  lgslem4  15751  lgsmod  15774  lgsdir2lem2  15777  lgsdir2  15781  lgsne0  15786  lgsmulsqcoprm  15794  lgseisenlem1  15818  2lgsoddprm  15861  2sqlem4  15866  wlk1walkdom  16229  wlkreslem  16248