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  806  eqtr3  2758  spc2ed  3543  elrab3t  3633  difprsnss  4744  elpw2g  5274  ideqg  5806  elrnmpt1s  5914  elrnmptg  5916  tz6.12-1  6863  eqfnfv2  6984  fmpt  7062  elunirn  7206  sucexeloni  7763  f1iun  7897  soseq  8109  tposfo2  8199  tposf12  8201  dom2lem  8939  ssnnfi  9104  ssfi  9107  enfii  9120  ac6sfi  9194  unfilem1  9215  pwfir  9227  nelaneq  9516  inf3lem2  9550  infdiffi  9579  dfac5lem5  10049  dfac2b  10053  dfac12k  10070  cfslb2n  10190  enfin2i  10243  fin23lem19  10258  axdc2lem  10370  axdc3lem4  10375  winainflem  10616  indpi  10830  ltexnq  10898  ltbtwnnq  10901  ltexprlem6  10964  prlem936  10970  elreal2  11055  fimaxre3  12102  addmodlteq  13908  expnbnd  14194  opfi1uzind  14473  repswswrd  14746  cshwidxmod  14765  climcnds  15816  fprod2dlem  15945  fprodle  15961  unbenlem  16879  acsfn  17625  lsmcv  21139  maducoeval2  22605  bastop2  22959  neipeltop  23094  rnelfmlem  23917  isfcls  23974  tgphaus  24082  mbfi1fseqlem4  25685  ulm2  26350  lgsqrmodndvds  27316  2lgsoddprm  27379  ax5seglem5  29002  wlkdlem4  29752  clwwlknonwwlknonb  30176  3wlkdlem4  30232  spanunsni  31650  nonbooli  31722  nmopun  32085  lncnopbd  32108  pjnmopi  32219  sumdmdlem  32489  disjun0  32665  rnmposs  32746  elrgspnlem2  33304  elrgspnlem3  33305  esumpcvgval  34222  bnj545  35037  bnj900  35071  bnj1498  35203  nummin  35236  fineqvac  35260  fineqvnttrclselem1  35265  noinfepfnregs  35276  wevgblacfn  35291  btwnconn1lem7  36275  ivthALT  36517  topfneec  36537  bj-elabd2ALT  37232  bj-snglss  37277  bj-elpwg  37359  bj-ideqg1ALT  37479  bj-imdiridlem  37499  mptsnunlem  37654  icoreresf  37668  lindsenlbs  37936  matunitlindf  37939  poimirlem14  37955  poimirlem22  37963  poimirlem26  37967  poimirlem29  37970  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  fdc  38066  ismtyres  38129  isdrngo3  38280  lshpset2N  39565  3dimlem1  39904  3dim3  39915  cdleme31fv2  40839  fsuppind  43023  isnumbasgrplem3  43533  pm13.13b  44835  ax6e2ndeqALT  45357  sineq0ALT  45363  elrnmpt1sf  45619  requad1  48098  clnbgrel  48304  nn0sumshdiglemB  49096  ipolubdm  49462  ipoglbdm  49465