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  3567  elrab3t  3658  difprsnss  4763  elpw2g  5288  ideqg  5815  elrnmpt1s  5923  elrnmptg  5925  tz6.12-1  6881  eqfnfv2  7004  fmpt  7082  elunirn  7225  sucexeloni  7785  f1iun  7922  soseq  8138  tposfo2  8228  tposf12  8230  dom2lem  8963  ssnnfi  9133  ssfi  9137  enfii  9150  ac6sfi  9231  unfilem1  9254  pwfir  9266  inf3lem2  9582  infdiffi  9611  dfac5lem5  10080  dfac2b  10084  dfac12k  10101  cfslb2n  10221  enfin2i  10274  fin23lem19  10289  axdc2lem  10401  axdc3lem4  10406  winainflem  10646  indpi  10860  ltexnq  10928  ltbtwnnq  10931  ltexprlem6  10994  prlem936  11000  elreal2  11085  fimaxre3  12129  addmodlteq  13911  expnbnd  14197  opfi1uzind  14476  repswswrd  14749  cshwidxmod  14768  climcnds  15817  fprod2dlem  15946  fprodle  15962  unbenlem  16879  acsfn  17620  lsmcv  21051  maducoeval2  22527  bastop2  22881  neipeltop  23016  rnelfmlem  23839  isfcls  23896  tgphaus  24004  mbfi1fseqlem4  25619  ulm2  26294  lgsqrmodndvds  27264  2lgsoddprm  27327  ax5seglem5  28860  wlkdlem4  29613  clwwlknonwwlknonb  30035  3wlkdlem4  30091  spanunsni  31508  nonbooli  31580  nmopun  31943  lncnopbd  31966  pjnmopi  32077  sumdmdlem  32347  disjun0  32524  rnmposs  32598  elrgspnlem2  33194  elrgspnlem3  33195  esumpcvgval  34068  bnj545  34885  bnj900  34919  bnj1498  35051  nummin  35081  fineqvac  35087  wevgblacfn  35096  btwnconn1lem7  36081  ivthALT  36323  topfneec  36343  bj-elabd2ALT  36913  bj-snglss  36958  bj-elpwg  37040  bj-ideqg1ALT  37153  bj-imdiridlem  37173  mptsnunlem  37326  icoreresf  37340  lindsenlbs  37609  matunitlindf  37612  poimirlem14  37628  poimirlem22  37636  poimirlem26  37640  poimirlem29  37643  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  fdc  37739  ismtyres  37802  isdrngo3  37953  lshpset2N  39112  3dimlem1  39452  3dim3  39463  cdleme31fv2  40387  fsuppind  42578  isnumbasgrplem3  43094  pm13.13b  44397  ax6e2ndeqALT  44920  sineq0ALT  44926  elrnmpt1sf  45183  requad1  47623  clnbgrel  47829  nn0sumshdiglemB  48609  ipolubdm  48975  ipoglbdm  48978