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  2762  spc2ed  3600  elrab3t  3690  difprsnss  4798  elpw2g  5332  ideqg  5861  elrnmpt1s  5969  elrnmptg  5971  tz6.12-1  6928  eqfnfv2  7051  fmpt  7129  elunirn  7272  sucexeloni  7830  f1iun  7969  soseq  8185  tposfo2  8275  tposf12  8277  dom2lem  9033  ssnnfi  9210  ssfi  9214  enfii  9227  ac6sfi  9321  unfilem1  9344  pwfir  9356  inf3lem2  9670  infdiffi  9699  dfac5lem5  10168  dfac2b  10172  dfac12k  10189  cfslb2n  10309  enfin2i  10362  fin23lem19  10377  axdc2lem  10489  axdc3lem4  10494  winainflem  10734  indpi  10948  ltexnq  11016  ltbtwnnq  11019  ltexprlem6  11082  prlem936  11088  elreal2  11173  fimaxre3  12215  addmodlteq  13988  expnbnd  14272  opfi1uzind  14551  repswswrd  14823  cshwidxmod  14842  climcnds  15888  fprod2dlem  16017  fprodle  16033  unbenlem  16947  acsfn  17703  lsmcv  21144  maducoeval2  22647  bastop2  23002  neipeltop  23138  rnelfmlem  23961  isfcls  24018  tgphaus  24126  mbfi1fseqlem4  25754  ulm2  26429  lgsqrmodndvds  27398  2lgsoddprm  27461  ax5seglem5  28949  wlkdlem4  29704  clwwlknonwwlknonb  30126  3wlkdlem4  30182  spanunsni  31599  nonbooli  31671  nmopun  32034  lncnopbd  32057  pjnmopi  32168  sumdmdlem  32438  disjun0  32609  rnmposs  32685  elrgspnlem2  33248  elrgspnlem3  33249  esumpcvgval  34080  bnj545  34910  bnj900  34944  bnj1498  35076  nummin  35106  fineqvac  35112  wevgblacfn  35115  btwnconn1lem7  36095  ivthALT  36337  topfneec  36357  bj-elabd2ALT  36927  bj-snglss  36972  bj-elpwg  37054  bj-ideqg1ALT  37167  bj-imdiridlem  37187  mptsnunlem  37340  icoreresf  37354  lindsenlbs  37623  matunitlindf  37626  poimirlem14  37642  poimirlem22  37650  poimirlem26  37654  poimirlem29  37657  ovoliunnfl  37670  voliunnfl  37672  volsupnfl  37673  fdc  37753  ismtyres  37816  isdrngo3  37967  lshpset2N  39121  3dimlem1  39461  3dim3  39472  cdleme31fv2  40396  fsuppind  42605  isnumbasgrplem3  43122  pm13.13b  44432  ax6e2ndeqALT  44956  sineq0ALT  44962  elrnmpt1sf  45199  requad1  47614  clnbgrel  47820  nn0sumshdiglemB  48546  ipolubdm  48891  ipoglbdm  48894