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  379  bitr  463  eqtr  2155  opabss  3987  euotd  4171  wetriext  4486  sosng  4607  xpsspw  4646  brcogw  4703  funimaexglem  5201  funfni  5218  fnco  5226  fnssres  5231  fn0  5237  fnimadisj  5238  fnimaeq0  5239  foco  5350  foimacnv  5378  fvelimab  5470  fvopab3ig  5488  dff3im  5558  dffo4  5561  fmptco  5579  f1eqcocnv  5685  f1ocnv2d  5967  fnexALT  6004  xp1st  6056  xp2nd  6057  tfrlemiubacc  6220  tfri2d  6226  tfr1onlemubacc  6236  tfrcllemubacc  6249  tfri3  6257  ecelqsg  6475  elqsn0m  6490  fidifsnen  6757  recclnq  7193  nq0a0  7258  qreccl  9427  difelfzle  9904  exfzdc  10010  modifeq2int  10152  frec2uzlt2d  10170  1elfz0hash  10545  caucvgrelemcau  10745  recvalap  10862  fzomaxdiflem  10877  2zsupmax  10990  fsumparts  11232  ntrivcvgap  11310  divconjdvds  11536  ndvdssub  11616  zsupcllemstep  11627  rplpwr  11704  dvdssqlem  11707  eucalgcvga  11728  mulgcddvds  11764  isprm2lem  11786  uniopn  12157  ntrval  12268  clsval  12269  neival  12301  restdis  12342  lmbrf  12373  cnpnei  12377  dviaddf  12827  dvimulf  12828