Theorem biimparc 480

Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimparc	⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Proof of Theorem biimparc

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprcd 249	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	imp 407	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  biantr  803  eqtr3  2764  spc2ed  3540  elrab3t  3623  difprsnss  4732  elpw2g  5268  ideqg  5760  elrnmpt1s  5866  elrnmptg  5868  eqfnfv2  6910  fmpt  6984  elunirn  7124  f1iun  7786  tposfo2  8065  tposf12  8067  dom2lem  8780  ssnnfi  8952  ssnnfiOLD  8953  ssfi  8956  pwfir  8959  enfii  8972  enfiiOLD  9039  ac6sfi  9058  unfilem1  9078  inf3lem2  9387  infdiffi  9416  dfac5lem5  9883  dfac2b  9886  dfac12k  9903  cfslb2n  10024  enfin2i  10077  fin23lem19  10092  axdc2lem  10204  axdc3lem4  10209  winainflem  10449  indpi  10663  ltexnq  10731  ltbtwnnq  10734  ltexprlem6  10797  prlem936  10803  elreal2  10888  fimaxre3  11921  addmodlteq  13666  expnbnd  13947  opfi1uzind  14215  repswswrd  14497  cshwidxmod  14516  climcnds  15563  fprod2dlem  15690  fprodle  15706  unbenlem  16609  acsfn  17368  lsmcv  20403  maducoeval2  21789  bastop2  22144  neipeltop  22280  rnelfmlem  23103  isfcls  23160  tgphaus  23268  mbfi1fseqlem4  24883  ulm2  25544  lgsqrmodndvds  26501  2lgsoddprm  26564  ax5seglem5  27301  wlkdlem4  28053  clwwlknonwwlknonb  28470  3wlkdlem4  28526  spanunsni  29941  nonbooli  30013  nmopun  30376  lncnopbd  30399  pjnmopi  30510  sumdmdlem  30780  disjun0  30934  rnmposs  31011  esumpcvgval  32046  bnj545  32875  bnj900  32909  bnj1498  33041  nummin  33063  fineqvac  33066  soseq  33803  btwnconn1lem7  34395  ivthALT  34524  topfneec  34544  bj-elabd2ALT  35113  bj-snglss  35160  bj-elpwg  35225  bj-ideqg1ALT  35336  bj-imdiridlem  35356  mptsnunlem  35509  icoreresf  35523  lindsenlbs  35772  matunitlindf  35775  poimirlem14  35791  poimirlem22  35799  poimirlem26  35803  poimirlem29  35806  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  fdc  35903  ismtyres  35966  isdrngo3  36117  lshpset2N  37133  3dimlem1  37472  3dim3  37483  cdleme31fv2  38407  fsuppind  40279  isnumbasgrplem3  40930  pm13.13b  42026  ax6e2ndeqALT  42551  sineq0ALT  42557  elrnmpt1sf  42727  requad1  45074  nn0sumshdiglemB  45966  ipolubdm  46273  ipoglbdm  46276