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  2784  spc2ed  3558  elrab3t  3647  difprsnss  4765  elpw2g  5302  ideqg  5835  elrnmpt1s  5947  elrnmptg  5949  tz6.12-1  6905  eqfnfv2  7027  fmpt  7107  elunirn  7252  sucexeloni  7812  f1iun  7945  soseq  8161  tposfo2  8251  tposf12  8253  dom2lem  9002  ssnnfi  9168  ssfi  9171  enfii  9184  ac6sfi  9258  unfilem1  9279  pwfir  9290  nelaneq  9578  inf3lem2  9612  infdiffi  9641  dfac5lem5  10134  dfac2b  10137  dfac12k  10154  cfslb2n  10274  enfin2i  10327  fin23lem19  10342  axdc2lem  10454  axdc3lem4  10459  winainflem  10706  indpi  10920  ltexnq  10988  ltbtwnnq  10991  ltexprlem6  11054  prlem936  11060  elreal2  11145  fimaxre3  12189  addmodlteq  14014  expnbnd  14300  opfi1uzind  14580  repswswrd  14859  cshwidxmod  14878  climcnds  15944  fprod2dlem  16073  fprodle  16089  unbenlem  17006  acsfn  17753  isdrng5  20923  lsmcv  21334  lindsenlbs  22070  maducoeval2  22868  matunitlindf  22909  bastop2  23225  neipeltop  23360  rnelfmlem  24184  isfcls  24241  tgphaus  24349  mbfi1fseqlem4  25952  ulm2  26628  lgsqrmodndvds  27597  2lgsoddprm  27660  ax5seglem5  29398  wlkdlem4  30151  clwwlknonwwlknonb  30584  3wlkdlem4  30650  spanunsni  32068  nonbooli  32140  nmopun  32503  lncnopbd  32526  pjnmopi  32637  sumdmdlem  32907  disjun0  33076  rnmposs  33154  elrgspnlem2  33691  elrgspnlem3  33692  esumpcvgval  34596  bnj545  35412  bnj900  35446  bnj1498  35578  nummin  35606  fineqvac  35650  fineqvnttrclselem1  35655  noinfepfnregs  35666  wevgblacfn  35716  btwnconn1lem7  36681  ivthALT  36962  topfneec  36982  bj-elabd2ALT  37677  bj-snglss  37722  bj-elpwg  37804  bj-ideqg1ALT  37925  bj-imdiridlem  37945  mptsnunlem  38100  icoreresf  38114  poimirlem14  38391  poimirlem22  38399  poimirlem26  38403  poimirlem29  38406  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  fdc  38503  ismtyres  38566  isdrngo3  38717  lshpset2N  40000  3dimlem1  40339  3dim3  40350  cdleme31fv2  41274  fsuppind  43444  isnumbasgrplem3  43954  pm13.13b  45240  ax6e2ndeqALT  45761  sineq0ALT  45767  elrnmpt1sf  46029  requad1  48546  clnbgrel  48752  nn0sumshdiglemB  49558  ipolubdm  49921  ipoglbdm  49924