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  2214  opabss  4098  euotd  4288  wetriext  4614  sosng  4737  xpsspw  4776  brcogw  4836  funimaexglem  5342  funfni  5359  fnco  5367  fnssres  5372  fn0  5378  fnimadisj  5379  fnimaeq0  5380  foco  5492  foimacnv  5523  fvelimab  5618  fvopab3ig  5636  dff3im  5708  dffo4  5711  fmptco  5729  f1eqcocnv  5839  f1ocnv2d  6129  fnexALT  6170  xp1st  6225  xp2nd  6226  tfrlemiubacc  6390  tfri2d  6396  tfr1onlemubacc  6406  tfrcllemubacc  6419  tfri3  6427  ecelqsg  6649  elqsn0m  6664  fidifsnen  6933  recclnq  7462  nq0a0  7527  qreccl  9719  difelfzle  10212  exfzdc  10319  zsupcllemstep  10322  modifeq2int  10481  frec2uzlt2d  10499  zzlesq  10803  1elfz0hash  10901  lennncl  10958  wrdsymb0  10970  caucvgrelemcau  11148  recvalap  11265  fzomaxdiflem  11280  2zsupmax  11394  2zinfmin  11411  fsumparts  11638  ntrivcvgap  11716  fsumdvds  12010  divconjdvds  12017  ndvdssub  12098  rplpwr  12205  dvdssqlem  12208  eucalgcvga  12237  mulgcddvds  12273  isprm2lem  12295  powm2modprm  12432  coprimeprodsq  12437  pythagtriplem11  12454  pythagtriplem13  12456  pcadd2  12521  4sqlem11  12581  grpidd  13052  ismndd  13104  gsumfzz  13153  gsumwmhm  13156  mulgaddcom  13302  resghm  13416  conjnsg  13437  isrngd  13535  isringd  13623  01eq0ring  13771  lspsneq0b  14009  lmodindp1  14010  znf1o  14233  uniopn  14263  ntrval  14372  clsval  14373  neival  14405  restdis  14446  lmbrf  14477  cnpnei  14481  dviaddf  14967  dvimulf  14968  logbgt0b  15228  perfectlem2  15262  lgslem4  15270  lgsmod  15293  lgsdir2lem2  15296  lgsdir2  15300  lgsne0  15305  lgsmulsqcoprm  15313  lgseisenlem1  15337  2lgsoddprm  15380  2sqlem4  15385