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  2761  spc2ed  3539  elrab3t  3628  difprsnss  4732  elpw2g  5261  ideqg  5793  elrnmpt1s  5901  elrnmptg  5903  tz6.12-1  6850  eqfnfv2  6972  fmpt  7051  elunirn  7195  sucexeloni  7752  f1iun  7886  soseq  8099  tposfo2  8189  tposf12  8191  dom2lem  8929  ssnnfi  9094  ssfi  9097  enfii  9110  ac6sfi  9184  unfilem1  9205  pwfir  9217  nelaneq  9507  inf3lem2  9541  infdiffi  9570  dfac5lem5  10040  dfac2b  10044  dfac12k  10061  cfslb2n  10181  enfin2i  10234  fin23lem19  10249  axdc2lem  10361  axdc3lem4  10366  winainflem  10607  indpi  10821  ltexnq  10889  ltbtwnnq  10892  ltexprlem6  10955  prlem936  10961  elreal2  11046  fimaxre3  12093  addmodlteq  13899  expnbnd  14185  opfi1uzind  14464  repswswrd  14737  cshwidxmod  14756  climcnds  15807  fprod2dlem  15936  fprodle  15952  unbenlem  16870  acsfn  17616  lsmcv  21134  maducoeval2  22623  bastop2  22977  neipeltop  23112  rnelfmlem  23935  isfcls  23992  tgphaus  24100  mbfi1fseqlem4  25703  ulm2  26368  lgsqrmodndvds  27334  2lgsoddprm  27397  ax5seglem5  29020  wlkdlem4  29770  clwwlknonwwlknonb  30194  3wlkdlem4  30250  spanunsni  31668  nonbooli  31740  nmopun  32103  lncnopbd  32126  pjnmopi  32237  sumdmdlem  32507  disjun0  32684  rnmposs  32765  elrgspnlem2  33324  elrgspnlem3  33325  esumpcvgval  34262  bnj545  35077  bnj900  35111  bnj1498  35243  nummin  35274  fineqvac  35297  fineqvnttrclselem1  35302  noinfepfnregs  35313  wevgblacfn  35337  btwnconn1lem7  36321  ivthALT  36563  topfneec  36583  bj-elabd2ALT  37278  bj-snglss  37323  bj-elpwg  37405  bj-ideqg1ALT  37525  bj-imdiridlem  37545  mptsnunlem  37700  icoreresf  37714  lindsenlbs  37982  matunitlindf  37985  poimirlem14  38001  poimirlem22  38009  poimirlem26  38013  poimirlem29  38016  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  fdc  38112  ismtyres  38175  isdrngo3  38326  lshpset2N  39611  3dimlem1  39950  3dim3  39961  cdleme31fv2  40885  fsuppind  43040  isnumbasgrplem3  43550  pm13.13b  44852  ax6e2ndeqALT  45374  sineq0ALT  45380  elrnmpt1sf  45636  requad1  48113  clnbgrel  48319  nn0sumshdiglemB  49111  ipolubdm  49477  ipoglbdm  49480