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  4158  euotd  4353  wetriext  4681  sosng  4805  xpsspw  4844  brcogw  4905  funimaexglem  5420  funfni  5439  fnco  5447  fnssres  5452  fn0  5459  fnimadisj  5460  fnimaeq0  5461  foco  5579  foimacnv  5610  fvelimab  5711  fvopab3ig  5729  dff3im  5800  dffo4  5803  fmptco  5821  f1eqcocnv  5942  f1ocnv2d  6237  fnexALT  6282  xp1st  6337  xp2nd  6338  tfrlemiubacc  6539  tfri2d  6545  tfr1onlemubacc  6555  tfrcllemubacc  6568  tfri3  6576  ecelqsg  6800  elqsn0m  6815  fidifsnen  7100  pr1or2  7442  recclnq  7655  nq0a0  7720  qreccl  9920  difelfzle  10414  exfzdc  10532  zsupcllemstep  10535  modifeq2int  10694  frec2uzlt2d  10712  zzlesq  11016  fihashgt0  11115  1elfz0hash  11116  lennncl  11182  wrdsymb0  11195  ccatsymb  11228  ccatlid  11232  ccatass  11234  ccatswrd  11300  swrdccat2  11301  ccatpfx  11331  swrdccatfn  11354  swrdccat  11365  caucvgrelemcau  11603  recvalap  11720  fzomaxdiflem  11735  2zsupmax  11849  2zinfmin  11866  fsumparts  12094  ntrivcvgap  12172  fsumdvds  12466  divconjdvds  12473  ndvdssub  12554  rplpwr  12661  dvdssqlem  12664  eucalgcvga  12693  mulgcddvds  12729  isprm2lem  12751  powm2modprm  12888  coprimeprodsq  12893  pythagtriplem11  12910  pythagtriplem13  12912  pcadd2  12977  4sqlem11  13037  grpidd  13529  ismndd  13583  gsumfzz  13641  gsumwmhm  13644  mulgaddcom  13796  resghm  13910  conjnsg  13931  isrngd  14030  isringd  14118  01eq0ring  14267  lspsneq0b  14506  lmodindp1  14507  znf1o  14730  psrgrp  14769  uniopn  14795  ntrval  14904  clsval  14905  neival  14937  restdis  14978  lmbrf  15009  cnpnei  15013  dviaddf  15499  dvimulf  15500  logbgt0b  15760  pellexlem2  15775  perfectlem2  15797  lgslem4  15805  lgsmod  15828  lgsdir2lem2  15831  lgsdir2  15835  lgsne0  15840  lgsmulsqcoprm  15848  lgseisenlem1  15872  2lgsoddprm  15915  2sqlem4  15920  wlk1walkdom  16283  wlkreslem  16302