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  2753  spc2ed  3556  elrab3t  3646  difprsnss  4751  elpw2g  5271  ideqg  5791  elrnmpt1s  5899  elrnmptg  5901  tz6.12-1  6845  eqfnfv2  6965  fmpt  7043  elunirn  7185  sucexeloni  7742  f1iun  7876  soseq  8089  tposfo2  8179  tposf12  8181  dom2lem  8914  ssnnfi  9079  ssfi  9082  enfii  9095  ac6sfi  9168  unfilem1  9189  pwfir  9201  inf3lem2  9519  infdiffi  9548  dfac5lem5  10015  dfac2b  10019  dfac12k  10036  cfslb2n  10156  enfin2i  10209  fin23lem19  10224  axdc2lem  10336  axdc3lem4  10341  winainflem  10581  indpi  10795  ltexnq  10863  ltbtwnnq  10866  ltexprlem6  10929  prlem936  10935  elreal2  11020  fimaxre3  12065  addmodlteq  13850  expnbnd  14136  opfi1uzind  14415  repswswrd  14688  cshwidxmod  14707  climcnds  15755  fprod2dlem  15884  fprodle  15900  unbenlem  16817  acsfn  17562  lsmcv  21076  maducoeval2  22553  bastop2  22907  neipeltop  23042  rnelfmlem  23865  isfcls  23922  tgphaus  24030  mbfi1fseqlem4  25644  ulm2  26319  lgsqrmodndvds  27289  2lgsoddprm  27352  ax5seglem5  28909  wlkdlem4  29660  clwwlknonwwlknonb  30081  3wlkdlem4  30137  spanunsni  31554  nonbooli  31626  nmopun  31989  lncnopbd  32012  pjnmopi  32123  sumdmdlem  32393  disjun0  32570  rnmposs  32651  elrgspnlem2  33205  elrgspnlem3  33206  esumpcvgval  34086  bnj545  34902  bnj900  34936  bnj1498  35068  nummin  35099  fineqvac  35127  fineqvnttrclselem1  35129  wevgblacfn  35141  btwnconn1lem7  36126  ivthALT  36368  topfneec  36388  bj-elabd2ALT  36958  bj-snglss  37003  bj-elpwg  37085  bj-ideqg1ALT  37198  bj-imdiridlem  37218  mptsnunlem  37371  icoreresf  37385  lindsenlbs  37654  matunitlindf  37657  poimirlem14  37673  poimirlem22  37681  poimirlem26  37685  poimirlem29  37688  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  fdc  37784  ismtyres  37847  isdrngo3  37998  lshpset2N  39157  3dimlem1  39496  3dim3  39507  cdleme31fv2  40431  fsuppind  42622  isnumbasgrplem3  43137  pm13.13b  44440  ax6e2ndeqALT  44962  sineq0ALT  44968  elrnmpt1sf  45225  requad1  47652  clnbgrel  47858  nn0sumshdiglemB  48651  ipolubdm  49017  ipoglbdm  49020