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  2760  spc2ed  3600  elrab3t  3693  difprsnss  4803  elpw2g  5338  ideqg  5864  elrnmpt1s  5972  elrnmptg  5974  tz6.12-1  6929  eqfnfv2  7051  fmpt  7129  elunirn  7270  sucexeloni  7828  f1iun  7966  soseq  8182  tposfo2  8272  tposf12  8274  dom2lem  9030  ssnnfi  9207  ssfi  9211  enfii  9223  ac6sfi  9317  unfilem1  9340  pwfir  9352  inf3lem2  9666  infdiffi  9695  dfac5lem5  10164  dfac2b  10168  dfac12k  10185  cfslb2n  10305  enfin2i  10358  fin23lem19  10373  axdc2lem  10485  axdc3lem4  10490  winainflem  10730  indpi  10944  ltexnq  11012  ltbtwnnq  11015  ltexprlem6  11078  prlem936  11084  elreal2  11169  fimaxre3  12211  addmodlteq  13983  expnbnd  14267  opfi1uzind  14546  repswswrd  14818  cshwidxmod  14837  climcnds  15883  fprod2dlem  16012  fprodle  16028  unbenlem  16941  acsfn  17703  lsmcv  21160  maducoeval2  22661  bastop2  23016  neipeltop  23152  rnelfmlem  23975  isfcls  24032  tgphaus  24140  mbfi1fseqlem4  25767  ulm2  26442  lgsqrmodndvds  27411  2lgsoddprm  27474  ax5seglem5  28962  wlkdlem4  29717  clwwlknonwwlknonb  30134  3wlkdlem4  30190  spanunsni  31607  nonbooli  31679  nmopun  32042  lncnopbd  32065  pjnmopi  32176  sumdmdlem  32446  disjun0  32614  rnmposs  32690  elrgspnlem2  33232  elrgspnlem3  33233  esumpcvgval  34058  bnj545  34887  bnj900  34921  bnj1498  35053  nummin  35083  fineqvac  35089  wevgblacfn  35092  btwnconn1lem7  36074  ivthALT  36317  topfneec  36337  bj-elabd2ALT  36907  bj-snglss  36952  bj-elpwg  37034  bj-ideqg1ALT  37147  bj-imdiridlem  37167  mptsnunlem  37320  icoreresf  37334  lindsenlbs  37601  matunitlindf  37604  poimirlem14  37620  poimirlem22  37628  poimirlem26  37632  poimirlem29  37635  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  fdc  37731  ismtyres  37794  isdrngo3  37945  lshpset2N  39100  3dimlem1  39440  3dim3  39451  cdleme31fv2  40375  fsuppind  42576  isnumbasgrplem3  43093  pm13.13b  44403  ax6e2ndeqALT  44928  sineq0ALT  44934  elrnmpt1sf  45131  requad1  47546  clnbgrel  47752  nn0sumshdiglemB  48469  ipolubdm  48775  ipoglbdm  48778