Theorem biimparc 484

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biantr  817  eqtr3  2787  spc2ed  3563  elrab3t  3652  difprsnss  4762  elpw2g  5294  ideqg  5828  elrnmpt1s  5940  elrnmptg  5942  tz6.12-1  6894  eqfnfv2  7016  fmpt  7095  elunirn  7239  sucexeloni  7796  f1iun  7929  soseq  8143  tposfo2  8233  tposf12  8235  dom2lem  8977  ssnnfi  9142  ssfi  9145  enfii  9158  ac6sfi  9232  unfilem1  9253  pwfir  9264  nelaneq  9552  inf3lem2  9586  infdiffi  9615  dfac5lem5  10099  dfac2b  10102  dfac12k  10119  cfslb2n  10240  enfin2i  10293  fin23lem19  10308  axdc2lem  10420  axdc3lem4  10425  winainflem  10666  indpi  10880  ltexnq  10948  ltbtwnnq  10951  ltexprlem6  11014  prlem936  11020  elreal2  11105  fimaxre3  12152  addmodlteq  13973  expnbnd  14259  opfi1uzind  14538  repswswrd  14811  cshwidxmod  14830  climcnds  15895  fprod2dlem  16024  fprodle  16040  unbenlem  16958  acsfn  17705  lsmcv  21234  maducoeval2  22758  bastop2  23112  neipeltop  23247  rnelfmlem  24070  isfcls  24127  tgphaus  24235  mbfi1fseqlem4  25838  ulm2  26506  lgsqrmodndvds  27475  2lgsoddprm  27538  ax5seglem5  29192  wlkdlem4  29942  clwwlknonwwlknonb  30366  3wlkdlem4  30422  spanunsni  31840  nonbooli  31912  nmopun  32275  lncnopbd  32298  pjnmopi  32409  sumdmdlem  32679  disjun0  32850  rnmposs  32930  elrgspnlem2  33476  elrgspnlem3  33477  esumpcvgval  34385  bnj545  35200  bnj900  35234  bnj1498  35366  nummin  35399  fineqvac  35424  fineqvnttrclselem1  35429  noinfepfnregs  35440  wevgblacfn  35466  btwnconn1lem7  36456  ivthALT  36708  topfneec  36728  bj-elabd2ALT  37422  bj-snglss  37467  bj-elpwg  37549  bj-ideqg1ALT  37669  bj-imdiridlem  37689  mptsnunlem  37844  icoreresf  37858  lindsenlbs  38126  matunitlindf  38129  poimirlem14  38145  poimirlem22  38153  poimirlem26  38157  poimirlem29  38160  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  fdc  38256  ismtyres  38319  isdrngo3  38470  lshpset2N  39755  3dimlem1  40094  3dim3  40105  cdleme31fv2  41029  fsuppind  43184  isnumbasgrplem3  43694  pm13.13b  44982  ax6e2ndeqALT  45504  sineq0ALT  45510  elrnmpt1sf  45765  requad1  48242  clnbgrel  48448  nn0sumshdiglemB  49251  ipolubdm  49616  ipoglbdm  49619