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  10486  zsupcllemstep  10489  modifeq2int  10648  frec2uzlt2d  10666  zzlesq  10970  fihashgt0  11069  1elfz0hash  11070  lennncl  11133  wrdsymb0  11146  ccatsymb  11179  ccatlid  11183  ccatass  11185  ccatswrd  11251  swrdccat2  11252  ccatpfx  11282  swrdccatfn  11305  swrdccat  11316  caucvgrelemcau  11541  recvalap  11658  fzomaxdiflem  11673  2zsupmax  11787  2zinfmin  11804  fsumparts  12032  ntrivcvgap  12110  fsumdvds  12404  divconjdvds  12411  ndvdssub  12492  rplpwr  12599  dvdssqlem  12602  eucalgcvga  12631  mulgcddvds  12667  isprm2lem  12689  powm2modprm  12826  coprimeprodsq  12831  pythagtriplem11  12848  pythagtriplem13  12850  pcadd2  12915  4sqlem11  12975  grpidd  13467  ismndd  13521  gsumfzz  13579  gsumwmhm  13582  mulgaddcom  13734  resghm  13848  conjnsg  13869  isrngd  13968  isringd  14056  01eq0ring  14205  lspsneq0b  14443  lmodindp1  14444  znf1o  14667  psrgrp  14701  uniopn  14727  ntrval  14836  clsval  14837  neival  14869  restdis  14910  lmbrf  14941  cnpnei  14945  dviaddf  15431  dvimulf  15432  logbgt0b  15692  perfectlem2  15726  lgslem4  15734  lgsmod  15757  lgsdir2lem2  15760  lgsdir2  15764  lgsne0  15769  lgsmulsqcoprm  15777  lgseisenlem1  15801  2lgsoddprm  15844  2sqlem4  15849  wlk1walkdom  16212  wlkreslem  16231