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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  biantr  811  eqtr3  2762  spc2ed  3546  elrab3t  3635  difprsnss  4739  elpw2g  5268  ideqg  5800  elrnmpt1s  5908  elrnmptg  5910  tz6.12-1  6857  eqfnfv2  6979  fmpt  7058  elunirn  7202  sucexeloni  7759  f1iun  7893  soseq  8106  tposfo2  8196  tposf12  8198  dom2lem  8936  ssnnfi  9101  ssfi  9104  enfii  9117  ac6sfi  9191  unfilem1  9212  pwfir  9224  nelaneq  9514  inf3lem2  9548  infdiffi  9577  dfac5lem5  10047  dfac2b  10051  dfac12k  10068  cfslb2n  10188  enfin2i  10241  fin23lem19  10256  axdc2lem  10368  axdc3lem4  10373  winainflem  10614  indpi  10828  ltexnq  10896  ltbtwnnq  10899  ltexprlem6  10962  prlem936  10968  elreal2  11053  fimaxre3  12100  addmodlteq  13906  expnbnd  14192  opfi1uzind  14471  repswswrd  14744  cshwidxmod  14763  climcnds  15814  fprod2dlem  15943  fprodle  15959  unbenlem  16877  acsfn  17623  lsmcv  21141  maducoeval2  22630  bastop2  22984  neipeltop  23119  rnelfmlem  23942  isfcls  23999  tgphaus  24107  mbfi1fseqlem4  25710  ulm2  26375  lgsqrmodndvds  27341  2lgsoddprm  27404  ax5seglem5  29027  wlkdlem4  29777  clwwlknonwwlknonb  30201  3wlkdlem4  30257  spanunsni  31675  nonbooli  31747  nmopun  32110  lncnopbd  32133  pjnmopi  32244  sumdmdlem  32514  disjun0  32691  rnmposs  32772  elrgspnlem2  33331  elrgspnlem3  33332  esumpcvgval  34269  bnj545  35084  bnj900  35118  bnj1498  35250  nummin  35281  fineqvac  35304  fineqvnttrclselem1  35309  noinfepfnregs  35320  wevgblacfn  35344  btwnconn1lem7  36328  ivthALT  36570  topfneec  36590  bj-elabd2ALT  37285  bj-snglss  37330  bj-elpwg  37412  bj-ideqg1ALT  37532  bj-imdiridlem  37552  mptsnunlem  37707  icoreresf  37721  lindsenlbs  37989  matunitlindf  37992  poimirlem14  38008  poimirlem22  38016  poimirlem26  38020  poimirlem29  38023  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  fdc  38119  ismtyres  38182  isdrngo3  38333  lshpset2N  39618  3dimlem1  39957  3dim3  39968  cdleme31fv2  40892  fsuppind  43047  isnumbasgrplem3  43557  pm13.13b  44859  ax6e2ndeqALT  45381  sineq0ALT  45387  elrnmpt1sf  45643  requad1  48120  clnbgrel  48326  nn0sumshdiglemB  49118  ipolubdm  49484  ipoglbdm  49487