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  2755  spc2ed  3552  elrab3t  3642  difprsnss  4750  elpw2g  5273  ideqg  5795  elrnmpt1s  5903  elrnmptg  5905  tz6.12-1  6851  eqfnfv2  6971  fmpt  7049  elunirn  7191  sucexeloni  7748  f1iun  7882  soseq  8095  tposfo2  8185  tposf12  8187  dom2lem  8921  ssnnfi  9086  ssfi  9089  enfii  9102  ac6sfi  9175  unfilem1  9196  pwfir  9208  inf3lem2  9526  infdiffi  9555  dfac5lem5  10025  dfac2b  10029  dfac12k  10046  cfslb2n  10166  enfin2i  10219  fin23lem19  10234  axdc2lem  10346  axdc3lem4  10351  winainflem  10591  indpi  10805  ltexnq  10873  ltbtwnnq  10876  ltexprlem6  10939  prlem936  10945  elreal2  11030  fimaxre3  12075  addmodlteq  13855  expnbnd  14141  opfi1uzind  14420  repswswrd  14693  cshwidxmod  14712  climcnds  15760  fprod2dlem  15889  fprodle  15905  unbenlem  16822  acsfn  17567  lsmcv  21080  maducoeval2  22556  bastop2  22910  neipeltop  23045  rnelfmlem  23868  isfcls  23925  tgphaus  24033  mbfi1fseqlem4  25647  ulm2  26322  lgsqrmodndvds  27292  2lgsoddprm  27355  ax5seglem5  28913  wlkdlem4  29664  clwwlknonwwlknonb  30088  3wlkdlem4  30144  spanunsni  31561  nonbooli  31633  nmopun  31996  lncnopbd  32019  pjnmopi  32130  sumdmdlem  32400  disjun0  32577  rnmposs  32658  elrgspnlem2  33217  elrgspnlem3  33218  esumpcvgval  34112  bnj545  34928  bnj900  34962  bnj1498  35094  nummin  35125  fineqvac  35160  fineqvnttrclselem1  35162  wevgblacfn  35174  btwnconn1lem7  36158  ivthALT  36400  topfneec  36420  bj-elabd2ALT  36990  bj-snglss  37035  bj-elpwg  37117  bj-ideqg1ALT  37230  bj-imdiridlem  37250  mptsnunlem  37403  icoreresf  37417  lindsenlbs  37675  matunitlindf  37678  poimirlem14  37694  poimirlem22  37702  poimirlem26  37706  poimirlem29  37709  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  fdc  37805  ismtyres  37868  isdrngo3  38019  lshpset2N  39238  3dimlem1  39577  3dim3  39588  cdleme31fv2  40512  fsuppind  42708  isnumbasgrplem3  43222  pm13.13b  44525  ax6e2ndeqALT  45047  sineq0ALT  45053  elrnmpt1sf  45310  requad1  47746  clnbgrel  47952  nn0sumshdiglemB  48745  ipolubdm  49111  ipoglbdm  49114