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  2766  spc2ed  3614  elrab3t  3707  difprsnss  4824  elpw2g  5351  ideqg  5876  elrnmpt1s  5982  elrnmptg  5984  tz6.12-1  6943  eqfnfv2  7065  fmpt  7144  elunirn  7288  sucexeloni  7845  f1iun  7984  soseq  8200  tposfo2  8290  tposf12  8292  dom2lem  9052  ssnnfi  9235  ssnnfiOLD  9236  ssfi  9240  enfii  9252  enfiiOLD  9327  ac6sfi  9348  unfilem1  9371  pwfir  9383  inf3lem2  9698  infdiffi  9727  dfac5lem5  10196  dfac2b  10200  dfac12k  10217  cfslb2n  10337  enfin2i  10390  fin23lem19  10405  axdc2lem  10517  axdc3lem4  10522  winainflem  10762  indpi  10976  ltexnq  11044  ltbtwnnq  11047  ltexprlem6  11110  prlem936  11116  elreal2  11201  fimaxre3  12241  addmodlteq  13997  expnbnd  14281  opfi1uzind  14560  repswswrd  14832  cshwidxmod  14851  climcnds  15899  fprod2dlem  16028  fprodle  16044  unbenlem  16955  acsfn  17717  lsmcv  21166  maducoeval2  22667  bastop2  23022  neipeltop  23158  rnelfmlem  23981  isfcls  24038  tgphaus  24146  mbfi1fseqlem4  25773  ulm2  26446  lgsqrmodndvds  27415  2lgsoddprm  27478  ax5seglem5  28966  wlkdlem4  29721  clwwlknonwwlknonb  30138  3wlkdlem4  30194  spanunsni  31611  nonbooli  31683  nmopun  32046  lncnopbd  32069  pjnmopi  32180  sumdmdlem  32450  disjun0  32617  rnmposs  32692  esumpcvgval  34042  bnj545  34871  bnj900  34905  bnj1498  35037  nummin  35067  fineqvac  35073  wevgblacfn  35076  btwnconn1lem7  36057  ivthALT  36301  topfneec  36321  bj-elabd2ALT  36891  bj-snglss  36936  bj-elpwg  37018  bj-ideqg1ALT  37131  bj-imdiridlem  37151  mptsnunlem  37304  icoreresf  37318  lindsenlbs  37575  matunitlindf  37578  poimirlem14  37594  poimirlem22  37602  poimirlem26  37606  poimirlem29  37609  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  fdc  37705  ismtyres  37768  isdrngo3  37919  lshpset2N  39075  3dimlem1  39415  3dim3  39426  cdleme31fv2  40350  fsuppind  42545  isnumbasgrplem3  43062  pm13.13b  44377  ax6e2ndeqALT  44902  sineq0ALT  44908  elrnmpt1sf  45096  requad1  47496  clnbgrel  47701  nn0sumshdiglemB  48354  ipolubdm  48659  ipoglbdm  48662