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  2224  opabss  4119  euotd  4312  wetriext  4638  sosng  4761  xpsspw  4800  brcogw  4860  funimaexglem  5371  funfni  5390  fnco  5398  fnssres  5403  fn0  5410  fnimadisj  5411  fnimaeq0  5412  foco  5526  foimacnv  5557  fvelimab  5653  fvopab3ig  5671  dff3im  5743  dffo4  5746  fmptco  5764  f1eqcocnv  5878  f1ocnv2d  6168  fnexALT  6214  xp1st  6269  xp2nd  6270  tfrlemiubacc  6434  tfri2d  6440  tfr1onlemubacc  6450  tfrcllemubacc  6463  tfri3  6471  ecelqsg  6693  elqsn0m  6708  fidifsnen  6988  pr1or2  7323  recclnq  7535  nq0a0  7600  qreccl  9793  difelfzle  10286  exfzdc  10401  zsupcllemstep  10404  modifeq2int  10563  frec2uzlt2d  10581  zzlesq  10885  1elfz0hash  10983  lennncl  11046  wrdsymb0  11058  ccatsymb  11091  ccatlid  11095  ccatass  11097  ccatswrd  11156  swrdccat2  11157  ccatpfx  11187  caucvgrelemcau  11376  recvalap  11493  fzomaxdiflem  11508  2zsupmax  11622  2zinfmin  11639  fsumparts  11866  ntrivcvgap  11944  fsumdvds  12238  divconjdvds  12245  ndvdssub  12326  rplpwr  12433  dvdssqlem  12436  eucalgcvga  12465  mulgcddvds  12501  isprm2lem  12523  powm2modprm  12660  coprimeprodsq  12665  pythagtriplem11  12682  pythagtriplem13  12684  pcadd2  12749  4sqlem11  12809  grpidd  13300  ismndd  13354  gsumfzz  13412  gsumwmhm  13415  mulgaddcom  13567  resghm  13681  conjnsg  13702  isrngd  13800  isringd  13888  01eq0ring  14036  lspsneq0b  14274  lmodindp1  14275  znf1o  14498  psrgrp  14532  uniopn  14558  ntrval  14667  clsval  14668  neival  14700  restdis  14741  lmbrf  14772  cnpnei  14776  dviaddf  15262  dvimulf  15263  logbgt0b  15523  perfectlem2  15557  lgslem4  15565  lgsmod  15588  lgsdir2lem2  15591  lgsdir2  15595  lgsne0  15600  lgsmulsqcoprm  15608  lgseisenlem1  15632  2lgsoddprm  15675  2sqlem4  15680