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  2222  opabss  4107  euotd  4298  wetriext  4624  sosng  4747  xpsspw  4786  brcogw  4846  funimaexglem  5356  funfni  5375  fnco  5383  fnssres  5388  fn0  5394  fnimadisj  5395  fnimaeq0  5396  foco  5508  foimacnv  5539  fvelimab  5634  fvopab3ig  5652  dff3im  5724  dffo4  5727  fmptco  5745  f1eqcocnv  5859  f1ocnv2d  6149  fnexALT  6195  xp1st  6250  xp2nd  6251  tfrlemiubacc  6415  tfri2d  6421  tfr1onlemubacc  6431  tfrcllemubacc  6444  tfri3  6452  ecelqsg  6674  elqsn0m  6689  fidifsnen  6966  recclnq  7504  nq0a0  7569  qreccl  9762  difelfzle  10255  exfzdc  10367  zsupcllemstep  10370  modifeq2int  10529  frec2uzlt2d  10547  zzlesq  10851  1elfz0hash  10949  lennncl  11012  wrdsymb0  11024  ccatsymb  11056  ccatlid  11060  ccatass  11062  caucvgrelemcau  11262  recvalap  11379  fzomaxdiflem  11394  2zsupmax  11508  2zinfmin  11525  fsumparts  11752  ntrivcvgap  11830  fsumdvds  12124  divconjdvds  12131  ndvdssub  12212  rplpwr  12319  dvdssqlem  12322  eucalgcvga  12351  mulgcddvds  12387  isprm2lem  12409  powm2modprm  12546  coprimeprodsq  12551  pythagtriplem11  12568  pythagtriplem13  12570  pcadd2  12635  4sqlem11  12695  grpidd  13186  ismndd  13240  gsumfzz  13298  gsumwmhm  13301  mulgaddcom  13453  resghm  13567  conjnsg  13588  isrngd  13686  isringd  13774  01eq0ring  13922  lspsneq0b  14160  lmodindp1  14161  znf1o  14384  psrgrp  14418  uniopn  14444  ntrval  14553  clsval  14554  neival  14586  restdis  14627  lmbrf  14658  cnpnei  14662  dviaddf  15148  dvimulf  15149  logbgt0b  15409  perfectlem2  15443  lgslem4  15451  lgsmod  15474  lgsdir2lem2  15477  lgsdir2  15481  lgsne0  15486  lgsmulsqcoprm  15494  lgseisenlem1  15518  2lgsoddprm  15561  2sqlem4  15566