Theorem biimparc 482

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  biantr  804  spc2ed  3602  elrab3t  3679  difprsnss  4732  elpw2g  5247  ideqg  5722  elrnmpt1s  5829  elrnmptg  5831  eqfnfv2  6803  fmpt  6874  elunirn  7010  f1iun  7645  tposfo2  7915  tposf12  7917  dom2lem  8549  enfii  8735  ssnnfi  8737  ac6sfi  8762  unfilem1  8782  inf3lem2  9092  infdiffi  9121  dfac5lem5  9553  dfac2b  9556  dfac12k  9573  cfslb2n  9690  enfin2i  9743  fin23lem19  9758  axdc2lem  9870  axdc3lem4  9875  winainflem  10115  indpi  10329  ltexnq  10397  ltbtwnnq  10400  ltexprlem6  10463  prlem936  10469  elreal2  10554  fimaxre3  11587  addmodlteq  13315  expnbnd  13594  opfi1uzind  13860  repswswrd  14146  cshwidxmod  14165  climcnds  15206  fprod2dlem  15334  fprodle  15350  unbenlem  16244  acsfn  16930  lsmcv  19913  maducoeval2  21249  bastop2  21602  neipeltop  21737  rnelfmlem  22560  isfcls  22617  tgphaus  22725  mbfi1fseqlem4  24319  ulm2  24973  lgsqrmodndvds  25929  2lgsoddprm  25992  ax5seglem5  26719  wlkdlem4  27467  clwwlknonwwlknonb  27885  3wlkdlem4  27941  spanunsni  29356  nonbooli  29428  nmopun  29791  lncnopbd  29814  pjnmopi  29925  sumdmdlem  30195  disjun0  30345  rnmposs  30419  esumpcvgval  31337  bnj545  32167  bnj900  32201  bnj1498  32333  soseq  33096  btwnconn1lem7  33554  ivthALT  33683  topfneec  33703  bj-snglss  34285  bj-elpwg  34348  bj-ideqg1ALT  34460  mptsnunlem  34622  icoreresf  34636  lindsenlbs  34902  matunitlindf  34905  poimirlem14  34921  poimirlem22  34929  poimirlem26  34933  poimirlem29  34936  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  fdc  35035  ismtyres  35101  isdrngo3  35252  lshpset2N  36270  3dimlem1  36609  3dim3  36620  cdleme31fv2  37544  isnumbasgrplem3  39725  pm13.13b  40760  ax6e2ndeqALT  41285  sineq0ALT  41291  elrnmpt1sf  41470  requad1  43807  nn0sumshdiglemB  44700