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  2782  spc2ed  3555  elrab3t  3643  difprsnss  4758  elpw2g  5294  ideqg  5828  elrnmpt1s  5940  elrnmptg  5942  tz6.12-1  6908  eqfnfv2  7030  fmpt  7110  elunirn  7255  sucexeloni  7823  f1iun  7956  soseq  8178  tposfo2  8269  tposf12  8271  dom2lem  9022  ssnnfi  9188  ssfi  9191  enfii  9204  ac6sfi  9278  unfilem1  9300  pwfir  9311  nelaneq  9599  inf3lem2  9633  infdiffi  9662  dfac5lem5  10209  dfac2b  10212  dfac12k  10229  cfslb2n  10349  enfin2i  10402  fin23lem19  10417  axdc2lem  10529  axdc3lem4  10534  winainflem  10781  indpi  10995  ltexnq  11063  ltbtwnnq  11066  ltexprlem6  11129  prlem936  11135  elreal2  11220  fimaxre3  12266  addmodlteq  14092  expnbnd  14379  opfi1uzind  14659  repswswrd  14939  cshwidxmod  14958  climcnds  16025  fprod2dlem  16152  fprodle  16168  unbenlem  17091  acsfn  17838  isdrng5  21013  lsmcv  21424  lindsenlbs  22162  maducoeval2  22960  matunitlindf  23001  bastop2  23317  neipeltop  23452  rnelfmlem  24276  isfcls  24333  tgphaus  24441  mbfi1fseqlem4  26044  ulm2  26717  lgsqrmodndvds  27685  2lgsoddprm  27748  ax5seglem5  29516  wlkdlem4  30269  clwwlknonwwlknonb  30702  3wlkdlem4  30768  spanunsni  32186  nonbooli  32258  nmopun  32621  lncnopbd  32644  pjnmopi  32755  sumdmdlem  33025  disjun0  33236  rnmposs  33314  elrgspnlem2  33850  elrgspnlem3  33851  esumpcvgval  34756  bnj545  35571  bnj900  35605  bnj1498  35737  nummin  35774  fineqvac  35840  fineqvnttrclselem1  35845  noinfepfnregs  35856  wevgblacfn  35958  btwnconn1lem7  36950  ivthALT  37215  topfneec  37235  bj-elabd2ALT  37930  bj-snglss  37975  bj-elpwg  38059  bj-ideqg1ALT  38179  bj-imdiridlem  38199  mptsnunlem  38354  icoreresf  38368  poimirlem14  38645  poimirlem22  38653  poimirlem26  38657  poimirlem29  38660  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  fdc  38772  ismtyres  38835  isdrngo3  38986  lshpset2N  40269  3dimlem1  40608  3dim3  40619  cdleme31fv2  41543  fsuppind  43711  isnumbasgrplem3  44200  pm13.13b  45485  ax6e2ndeqALT  46006  sineq0ALT  46012  elrnmpt1sf  46297  requad1  48813  clnbgrel  49019  nn0sumshdiglemB  49825  ipolubdm  50194  ipoglbdm  50197