Theorem biimpar 295

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 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imp 123	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exbiri  380  bitr  464  eqtr  2175  opabss  4028  euotd  4214  wetriext  4536  sosng  4659  xpsspw  4698  brcogw  4755  funimaexglem  5253  funfni  5270  fnco  5278  fnssres  5283  fn0  5289  fnimadisj  5290  fnimaeq0  5291  foco  5402  foimacnv  5432  fvelimab  5524  fvopab3ig  5542  dff3im  5612  dffo4  5615  fmptco  5633  f1eqcocnv  5741  f1ocnv2d  6024  fnexALT  6061  xp1st  6113  xp2nd  6114  tfrlemiubacc  6277  tfri2d  6283  tfr1onlemubacc  6293  tfrcllemubacc  6306  tfri3  6314  ecelqsg  6533  elqsn0m  6548  fidifsnen  6815  recclnq  7312  nq0a0  7377  qreccl  9551  difelfzle  10033  exfzdc  10139  modifeq2int  10285  frec2uzlt2d  10303  1elfz0hash  10680  caucvgrelemcau  10880  recvalap  10997  fzomaxdiflem  11012  2zsupmax  11125  fsumparts  11367  ntrivcvgap  11445  divconjdvds  11741  ndvdssub  11821  zsupcllemstep  11832  rplpwr  11911  dvdssqlem  11914  eucalgcvga  11935  mulgcddvds  11971  isprm2lem  11993  powm2modprm  12127  uniopn  12410  ntrval  12521  clsval  12522  neival  12554  restdis  12595  lmbrf  12626  cnpnei  12630  dviaddf  13080  dvimulf  13081  logbgt0b  13294