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  2158  opabss  4000  euotd  4184  wetriext  4499  sosng  4620  xpsspw  4659  brcogw  4716  funimaexglem  5214  funfni  5231  fnco  5239  fnssres  5244  fn0  5250  fnimadisj  5251  fnimaeq0  5252  foco  5363  foimacnv  5393  fvelimab  5485  fvopab3ig  5503  dff3im  5573  dffo4  5576  fmptco  5594  f1eqcocnv  5700  f1ocnv2d  5982  fnexALT  6019  xp1st  6071  xp2nd  6072  tfrlemiubacc  6235  tfri2d  6241  tfr1onlemubacc  6251  tfrcllemubacc  6264  tfri3  6272  ecelqsg  6490  elqsn0m  6505  fidifsnen  6772  recclnq  7224  nq0a0  7289  qreccl  9461  difelfzle  9942  exfzdc  10048  modifeq2int  10190  frec2uzlt2d  10208  1elfz0hash  10584  caucvgrelemcau  10784  recvalap  10901  fzomaxdiflem  10916  2zsupmax  11029  fsumparts  11271  ntrivcvgap  11349  divconjdvds  11583  ndvdssub  11663  zsupcllemstep  11674  rplpwr  11751  dvdssqlem  11754  eucalgcvga  11775  mulgcddvds  11811  isprm2lem  11833  uniopn  12207  ntrval  12318  clsval  12319  neival  12351  restdis  12392  lmbrf  12423  cnpnei  12427  dviaddf  12877  dvimulf  12878  logbgt0b  13091