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  805  eqtr3  2758  spc2ed  3585  elrab3t  3675  difprsnss  4780  elpw2g  5308  ideqg  5836  elrnmpt1s  5944  elrnmptg  5946  tz6.12-1  6904  eqfnfv2  7027  fmpt  7105  elunirn  7248  sucexeloni  7808  f1iun  7947  soseq  8163  tposfo2  8253  tposf12  8255  dom2lem  9011  ssnnfi  9188  ssfi  9192  enfii  9205  ac6sfi  9297  unfilem1  9320  pwfir  9332  inf3lem2  9648  infdiffi  9677  dfac5lem5  10146  dfac2b  10150  dfac12k  10167  cfslb2n  10287  enfin2i  10340  fin23lem19  10355  axdc2lem  10467  axdc3lem4  10472  winainflem  10712  indpi  10926  ltexnq  10994  ltbtwnnq  10997  ltexprlem6  11060  prlem936  11066  elreal2  11151  fimaxre3  12193  addmodlteq  13969  expnbnd  14255  opfi1uzind  14534  repswswrd  14807  cshwidxmod  14826  climcnds  15872  fprod2dlem  16001  fprodle  16017  unbenlem  16933  acsfn  17676  lsmcv  21107  maducoeval2  22583  bastop2  22937  neipeltop  23072  rnelfmlem  23895  isfcls  23952  tgphaus  24060  mbfi1fseqlem4  25676  ulm2  26351  lgsqrmodndvds  27321  2lgsoddprm  27384  ax5seglem5  28917  wlkdlem4  29670  clwwlknonwwlknonb  30092  3wlkdlem4  30148  spanunsni  31565  nonbooli  31637  nmopun  32000  lncnopbd  32023  pjnmopi  32134  sumdmdlem  32404  disjun0  32581  rnmposs  32657  elrgspnlem2  33243  elrgspnlem3  33244  esumpcvgval  34114  bnj545  34931  bnj900  34965  bnj1498  35097  nummin  35127  fineqvac  35133  wevgblacfn  35136  btwnconn1lem7  36116  ivthALT  36358  topfneec  36378  bj-elabd2ALT  36948  bj-snglss  36993  bj-elpwg  37075  bj-ideqg1ALT  37188  bj-imdiridlem  37208  mptsnunlem  37361  icoreresf  37375  lindsenlbs  37644  matunitlindf  37647  poimirlem14  37663  poimirlem22  37671  poimirlem26  37675  poimirlem29  37678  ovoliunnfl  37691  voliunnfl  37693  volsupnfl  37694  fdc  37774  ismtyres  37837  isdrngo3  37988  lshpset2N  39142  3dimlem1  39482  3dim3  39493  cdleme31fv2  40417  fsuppind  42588  isnumbasgrplem3  43104  pm13.13b  44407  ax6e2ndeqALT  44930  sineq0ALT  44936  elrnmpt1sf  45193  requad1  47616  clnbgrel  47822  nn0sumshdiglemB  48580  ipolubdm  48941  ipoglbdm  48944