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  2751  spc2ed  3558  elrab3t  3649  difprsnss  4753  elpw2g  5275  ideqg  5798  elrnmpt1s  5905  elrnmptg  5907  tz6.12-1  6849  eqfnfv2  6970  fmpt  7048  elunirn  7191  sucexeloni  7749  f1iun  7886  soseq  8099  tposfo2  8189  tposf12  8191  dom2lem  8924  ssnnfi  9093  ssfi  9097  enfii  9110  ac6sfi  9189  unfilem1  9212  pwfir  9224  inf3lem2  9544  infdiffi  9573  dfac5lem5  10040  dfac2b  10044  dfac12k  10061  cfslb2n  10181  enfin2i  10234  fin23lem19  10249  axdc2lem  10361  axdc3lem4  10366  winainflem  10606  indpi  10820  ltexnq  10888  ltbtwnnq  10891  ltexprlem6  10954  prlem936  10960  elreal2  11045  fimaxre3  12089  addmodlteq  13871  expnbnd  14157  opfi1uzind  14436  repswswrd  14708  cshwidxmod  14727  climcnds  15776  fprod2dlem  15905  fprodle  15921  unbenlem  16838  acsfn  17583  lsmcv  21066  maducoeval2  22543  bastop2  22897  neipeltop  23032  rnelfmlem  23855  isfcls  23912  tgphaus  24020  mbfi1fseqlem4  25635  ulm2  26310  lgsqrmodndvds  27280  2lgsoddprm  27343  ax5seglem5  28896  wlkdlem4  29647  clwwlknonwwlknonb  30068  3wlkdlem4  30124  spanunsni  31541  nonbooli  31613  nmopun  31976  lncnopbd  31999  pjnmopi  32110  sumdmdlem  32380  disjun0  32557  rnmposs  32631  elrgspnlem2  33193  elrgspnlem3  33194  esumpcvgval  34044  bnj545  34861  bnj900  34895  bnj1498  35027  nummin  35057  fineqvac  35071  wevgblacfn  35081  btwnconn1lem7  36066  ivthALT  36308  topfneec  36328  bj-elabd2ALT  36898  bj-snglss  36943  bj-elpwg  37025  bj-ideqg1ALT  37138  bj-imdiridlem  37158  mptsnunlem  37311  icoreresf  37325  lindsenlbs  37594  matunitlindf  37597  poimirlem14  37613  poimirlem22  37621  poimirlem26  37625  poimirlem29  37628  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  fdc  37724  ismtyres  37787  isdrngo3  37938  lshpset2N  39097  3dimlem1  39437  3dim3  39448  cdleme31fv2  40372  fsuppind  42563  isnumbasgrplem3  43078  pm13.13b  44381  ax6e2ndeqALT  44904  sineq0ALT  44910  elrnmpt1sf  45167  requad1  47607  clnbgrel  47813  nn0sumshdiglemB  48606  ipolubdm  48972  ipoglbdm  48975