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  2223  opabss  4108  euotd  4299  wetriext  4625  sosng  4748  xpsspw  4787  brcogw  4847  funimaexglem  5357  funfni  5376  fnco  5384  fnssres  5389  fn0  5395  fnimadisj  5396  fnimaeq0  5397  foco  5509  foimacnv  5540  fvelimab  5635  fvopab3ig  5653  dff3im  5725  dffo4  5728  fmptco  5746  f1eqcocnv  5860  f1ocnv2d  6150  fnexALT  6196  xp1st  6251  xp2nd  6252  tfrlemiubacc  6416  tfri2d  6422  tfr1onlemubacc  6432  tfrcllemubacc  6445  tfri3  6453  ecelqsg  6675  elqsn0m  6690  fidifsnen  6967  recclnq  7505  nq0a0  7570  qreccl  9763  difelfzle  10256  exfzdc  10369  zsupcllemstep  10372  modifeq2int  10531  frec2uzlt2d  10549  zzlesq  10853  1elfz0hash  10951  lennncl  11014  wrdsymb0  11026  ccatsymb  11058  ccatlid  11062  ccatass  11064  ccatswrd  11123  swrdccat2  11124  caucvgrelemcau  11291  recvalap  11408  fzomaxdiflem  11423  2zsupmax  11537  2zinfmin  11554  fsumparts  11781  ntrivcvgap  11859  fsumdvds  12153  divconjdvds  12160  ndvdssub  12241  rplpwr  12348  dvdssqlem  12351  eucalgcvga  12380  mulgcddvds  12416  isprm2lem  12438  powm2modprm  12575  coprimeprodsq  12580  pythagtriplem11  12597  pythagtriplem13  12599  pcadd2  12664  4sqlem11  12724  grpidd  13215  ismndd  13269  gsumfzz  13327  gsumwmhm  13330  mulgaddcom  13482  resghm  13596  conjnsg  13617  isrngd  13715  isringd  13803  01eq0ring  13951  lspsneq0b  14189  lmodindp1  14190  znf1o  14413  psrgrp  14447  uniopn  14473  ntrval  14582  clsval  14583  neival  14615  restdis  14656  lmbrf  14687  cnpnei  14691  dviaddf  15177  dvimulf  15178  logbgt0b  15438  perfectlem2  15472  lgslem4  15480  lgsmod  15503  lgsdir2lem2  15506  lgsdir2  15510  lgsne0  15515  lgsmulsqcoprm  15523  lgseisenlem1  15547  2lgsoddprm  15590  2sqlem4  15595