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  2207  opabss  4082  euotd  4269  wetriext  4591  sosng  4714  xpsspw  4753  brcogw  4811  funimaexglem  5314  funfni  5331  fnco  5339  fnssres  5344  fn0  5350  fnimadisj  5351  fnimaeq0  5352  foco  5463  foimacnv  5494  fvelimab  5588  fvopab3ig  5606  dff3im  5677  dffo4  5680  fmptco  5698  f1eqcocnv  5808  f1ocnv2d  6093  fnexALT  6130  xp1st  6184  xp2nd  6185  tfrlemiubacc  6349  tfri2d  6355  tfr1onlemubacc  6365  tfrcllemubacc  6378  tfri3  6386  ecelqsg  6606  elqsn0m  6621  fidifsnen  6888  recclnq  7409  nq0a0  7474  qreccl  9660  difelfzle  10152  exfzdc  10258  modifeq2int  10404  frec2uzlt2d  10422  1elfz0hash  10804  caucvgrelemcau  11007  recvalap  11124  fzomaxdiflem  11139  2zsupmax  11252  2zinfmin  11269  fsumparts  11496  ntrivcvgap  11574  divconjdvds  11873  ndvdssub  11953  zsupcllemstep  11964  rplpwr  12046  dvdssqlem  12049  eucalgcvga  12076  mulgcddvds  12112  isprm2lem  12134  powm2modprm  12270  coprimeprodsq  12275  pythagtriplem11  12292  pythagtriplem13  12294  grpidd  12825  ismndd  12864  mulgaddcom  13052  resghm  13160  conjnsg  13181  isrngd  13268  isringd  13356  01eq0ring  13497  lspsneq0b  13704  lmodindp1  13705  uniopn  13885  ntrval  13994  clsval  13995  neival  14027  restdis  14068  lmbrf  14099  cnpnei  14103  dviaddf  14553  dvimulf  14554  logbgt0b  14768  lgslem4  14788  lgsmod  14811  lgsdir2lem2  14814  lgsdir2  14818  lgsne0  14823  lgsmulsqcoprm  14831  lgseisenlem1  14834  2sqlem4  14849