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  2783  spc2ed  3556  elrab3t  3644  difprsnss  4762  elpw2g  5295  ideqg  5829  elrnmpt1s  5941  elrnmptg  5943  tz6.12-1  6900  eqfnfv2  7022  fmpt  7102  elunirn  7247  sucexeloni  7812  f1iun  7945  soseq  8160  tposfo2  8250  tposf12  8252  dom2lem  9003  ssnnfi  9169  ssfi  9172  enfii  9185  ac6sfi  9259  unfilem1  9281  pwfir  9292  nelaneq  9580  inf3lem2  9614  infdiffi  9643  dfac5lem5  10187  dfac2b  10190  dfac12k  10207  cfslb2n  10327  enfin2i  10380  fin23lem19  10395  axdc2lem  10507  axdc3lem4  10512  winainflem  10759  indpi  10973  ltexnq  11041  ltbtwnnq  11044  ltexprlem6  11107  prlem936  11113  elreal2  11198  fimaxre3  12244  addmodlteq  14069  expnbnd  14356  opfi1uzind  14636  repswswrd  14915  cshwidxmod  14934  climcnds  16000  fprod2dlem  16127  fprodle  16143  unbenlem  17066  acsfn  17813  isdrng5  20988  lsmcv  21399  lindsenlbs  22137  maducoeval2  22935  matunitlindf  22976  bastop2  23292  neipeltop  23427  rnelfmlem  24251  isfcls  24308  tgphaus  24416  mbfi1fseqlem4  26019  ulm2  26694  lgsqrmodndvds  27662  2lgsoddprm  27725  ax5seglem5  29493  wlkdlem4  30246  clwwlknonwwlknonb  30679  3wlkdlem4  30745  spanunsni  32163  nonbooli  32235  nmopun  32598  lncnopbd  32621  pjnmopi  32732  sumdmdlem  33002  disjun0  33171  rnmposs  33249  elrgspnlem2  33786  elrgspnlem3  33787  esumpcvgval  34692  bnj545  35508  bnj900  35542  bnj1498  35674  nummin  35701  fineqvac  35757  fineqvnttrclselem1  35762  noinfepfnregs  35773  wevgblacfn  35863  btwnconn1lem7  36828  ivthALT  37093  topfneec  37113  bj-elabd2ALT  37808  bj-snglss  37853  bj-elpwg  37935  bj-ideqg1ALT  38054  bj-imdiridlem  38074  mptsnunlem  38229  icoreresf  38243  poimirlem14  38520  poimirlem22  38528  poimirlem26  38532  poimirlem29  38535  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  fdc  38647  ismtyres  38710  isdrngo3  38861  lshpset2N  40144  3dimlem1  40483  3dim3  40494  cdleme31fv2  41418  fsuppind  43580  isnumbasgrplem3  44065  pm13.13b  45351  ax6e2ndeqALT  45872  sineq0ALT  45878  elrnmpt1sf  46147  requad1  48664  clnbgrel  48870  nn0sumshdiglemB  49676  ipolubdm  50039  ipoglbdm  50042