Theorem biimparc 484

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biantr  806  spc2ed  3518  elrab3t  3599  difprsnss  4682  elpw2g  5207  ideqg  5684  elrnmpt1s  5791  elrnmptg  5793  eqfnfv2  6787  fmpt  6858  elunirn  6995  f1iun  7642  tposfo2  7918  tposf12  7920  dom2lem  8560  enfii  8749  ssnnfi  8751  ac6sfi  8780  unfilem1  8800  inf3lem2  9110  infdiffi  9139  dfac5lem5  9572  dfac2b  9575  dfac12k  9592  cfslb2n  9713  enfin2i  9766  fin23lem19  9781  axdc2lem  9893  axdc3lem4  9898  winainflem  10138  indpi  10352  ltexnq  10420  ltbtwnnq  10423  ltexprlem6  10486  prlem936  10492  elreal2  10577  fimaxre3  11609  addmodlteq  13348  expnbnd  13628  opfi1uzind  13896  repswswrd  14178  cshwidxmod  14197  climcnds  15239  fprod2dlem  15367  fprodle  15383  unbenlem  16284  acsfn  16973  lsmcv  19966  maducoeval2  21325  bastop2  21679  neipeltop  21814  rnelfmlem  22637  isfcls  22694  tgphaus  22802  mbfi1fseqlem4  24403  ulm2  25064  lgsqrmodndvds  26021  2lgsoddprm  26084  ax5seglem5  26811  wlkdlem4  27559  clwwlknonwwlknonb  27975  3wlkdlem4  28031  spanunsni  29446  nonbooli  29518  nmopun  29881  lncnopbd  29904  pjnmopi  30015  sumdmdlem  30285  disjun0  30441  rnmposs  30520  esumpcvgval  31550  bnj545  32380  bnj900  32414  bnj1498  32546  nummin  32577  soseq  33342  btwnconn1lem7  33929  ivthALT  34058  topfneec  34078  bj-snglss  34672  bj-elpwg  34736  bj-ideqg1ALT  34845  bj-imdiridlem  34865  mptsnunlem  35020  icoreresf  35034  lindsenlbs  35317  matunitlindf  35320  poimirlem14  35336  poimirlem22  35344  poimirlem26  35348  poimirlem29  35351  ovoliunnfl  35364  voliunnfl  35366  volsupnfl  35367  fdc  35448  ismtyres  35511  isdrngo3  35662  lshpset2N  36680  3dimlem1  37019  3dim3  37030  cdleme31fv2  37954  fsuppind  39769  isnumbasgrplem3  40407  pm13.13b  41470  ax6e2ndeqALT  41995  sineq0ALT  42001  elrnmpt1sf  42171  requad1  44492  nn0sumshdiglemB  45384