Theorem biimparc 479

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  biantr  806  eqtr3  2759  spc2ed  3557  elrab3t  3647  difprsnss  4757  elpw2g  5280  ideqg  5808  elrnmpt1s  5916  elrnmptg  5918  tz6.12-1  6865  eqfnfv2  6986  fmpt  7064  elunirn  7207  sucexeloni  7764  f1iun  7898  soseq  8111  tposfo2  8201  tposf12  8203  dom2lem  8941  ssnnfi  9106  ssfi  9109  enfii  9122  ac6sfi  9196  unfilem1  9217  pwfir  9229  inf3lem2  9550  infdiffi  9579  dfac5lem5  10049  dfac2b  10053  dfac12k  10070  cfslb2n  10190  enfin2i  10243  fin23lem19  10258  axdc2lem  10370  axdc3lem4  10375  winainflem  10616  indpi  10830  ltexnq  10898  ltbtwnnq  10901  ltexprlem6  10964  prlem936  10970  elreal2  11055  fimaxre3  12100  addmodlteq  13881  expnbnd  14167  opfi1uzind  14446  repswswrd  14719  cshwidxmod  14738  climcnds  15786  fprod2dlem  15915  fprodle  15931  unbenlem  16848  acsfn  17594  lsmcv  21108  maducoeval2  22596  bastop2  22950  neipeltop  23085  rnelfmlem  23908  isfcls  23965  tgphaus  24073  mbfi1fseqlem4  25687  ulm2  26362  lgsqrmodndvds  27332  2lgsoddprm  27395  ax5seglem5  29018  wlkdlem4  29769  clwwlknonwwlknonb  30193  3wlkdlem4  30249  spanunsni  31666  nonbooli  31738  nmopun  32101  lncnopbd  32124  pjnmopi  32235  sumdmdlem  32505  disjun0  32681  rnmposs  32762  elrgspnlem2  33336  elrgspnlem3  33337  esumpcvgval  34255  bnj545  35070  bnj900  35104  bnj1498  35236  nummin  35268  fineqvac  35291  fineqvnttrclselem1  35296  noinfepfnregs  35307  wevgblacfn  35322  btwnconn1lem7  36306  ivthALT  36548  topfneec  36568  bj-elabd2ALT  37167  bj-snglss  37212  bj-elpwg  37294  bj-ideqg1ALT  37414  bj-imdiridlem  37434  mptsnunlem  37587  icoreresf  37601  lindsenlbs  37860  matunitlindf  37863  poimirlem14  37879  poimirlem22  37887  poimirlem26  37891  poimirlem29  37894  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  fdc  37990  ismtyres  38053  isdrngo3  38204  lshpset2N  39489  3dimlem1  39828  3dim3  39839  cdleme31fv2  40763  fsuppind  42942  isnumbasgrplem3  43456  pm13.13b  44758  ax6e2ndeqALT  45280  sineq0ALT  45286  elrnmpt1sf  45542  requad1  47976  clnbgrel  48182  nn0sumshdiglemB  48974  ipolubdm  49340  ipoglbdm  49343