Theorem biimparc 485

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 253	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	imp 412	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biantr  818  eqtr3  2785  spc2ed  3559  elrab3t  3647  difprsnss  4762  elpw2g  5299  ideqg  5835  elrnmpt1s  5948  elrnmptg  5950  tz6.12-1  6931  eqfnfv2  7053  fmpt  7134  elunirn  7278  rnmposs  7578  sucexeloni  7847  f1iun  7980  soseq  8203  tposfo2  8294  tposf12  8296  dom2lem  9047  ssnnfi  9213  ssfi  9216  enfii  9229  ac6sfi  9303  unfilem1  9325  pwfir  9336  nelaneq  9623  inf3lem2  9657  infdiffi  9686  dfac5lem5  10233  dfac2b  10236  dfac12k  10253  cfslb2n  10373  enfin2i  10426  fin23lem19  10441  axdc2lem  10553  axdc3lem4  10558  winainflem  10805  indpi  11019  ltexnq  11087  ltbtwnnq  11090  ltexprlem6  11153  prlem936  11159  elreal2  11244  fimaxre3  12290  addmodlteq  14116  expnbnd  14403  opfi1uzind  14683  repswswrd  14963  cshwidxmod  14982  climcnds  16049  fprod2dlem  16176  fprodle  16192  unbenlem  17115  acsfn  17862  isdrng5  21038  lsmcv  21449  lindsenlbs  22187  maducoeval2  22985  matunitlindf  23026  bastop2  23342  neipeltop  23477  rnelfmlem  24301  isfcls  24358  tgphaus  24466  mbfi1fseqlem4  26069  ulm2  26742  lgsqrmodndvds  27710  2lgsoddprm  27773  ax5seglem5  29541  wlkdlem4  30294  clwwlknonwwlknonb  30727  3wlkdlem4  30793  spanunsni  32211  nonbooli  32283  nmopun  32646  lncnopbd  32669  pjnmopi  32780  sumdmdlem  33050  disjun0  33261  elrgspnlem2  33874  elrgspnlem3  33875  esumpcvgval  34780  bnj545  35595  bnj900  35629  bnj1498  35761  nummin  35806  fineqvac  35884  fineqvnttrclselem1  35889  noinfepfnregs  35900  wevgblacfn  36039  btwnconn1lem7  37036  ivthALT  37301  topfneec  37321  bj-elabd2ALT  38016  bj-snglss  38061  bj-elpwg  38158  bj-ideqg1ALT  38278  bj-imdiridlem  38298  mptsnunlem  38453  icoreresf  38467  poimirlem14  38744  poimirlem22  38752  poimirlem26  38756  poimirlem29  38759  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  fdc  38871  ismtyres  38934  isdrngo3  39085  lshpset2N  40368  3dimlem1  40707  3dim3  40718  cdleme31fv2  41642  fsuppind  43811  isnumbasgrplem3  44299  pm13.13b  45584  ax6e2ndeqALT  46104  sineq0ALT  46110  elrnmpt1sf  46409  requad1  48925  clnbgrel  49131  nn0sumshdiglemB  49937  ipolubdm  50306  ipoglbdm  50309