Theorem biimparc 483

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 410	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  biantr  805  spc2ed  3550  elrab3t  3627  difprsnss  4692  elpw2g  5211  ideqg  5686  elrnmpt1s  5793  elrnmptg  5795  eqfnfv2  6780  fmpt  6851  elunirn  6988  f1iun  7627  tposfo2  7898  tposf12  7900  dom2lem  8532  enfii  8719  ssnnfi  8721  ac6sfi  8746  unfilem1  8766  inf3lem2  9076  infdiffi  9105  dfac5lem5  9538  dfac2b  9541  dfac12k  9558  cfslb2n  9679  enfin2i  9732  fin23lem19  9747  axdc2lem  9859  axdc3lem4  9864  winainflem  10104  indpi  10318  ltexnq  10386  ltbtwnnq  10389  ltexprlem6  10452  prlem936  10458  elreal2  10543  fimaxre3  11575  addmodlteq  13309  expnbnd  13589  opfi1uzind  13855  repswswrd  14137  cshwidxmod  14156  climcnds  15198  fprod2dlem  15326  fprodle  15342  unbenlem  16234  acsfn  16922  lsmcv  19906  maducoeval2  21245  bastop2  21599  neipeltop  21734  rnelfmlem  22557  isfcls  22614  tgphaus  22722  mbfi1fseqlem4  24322  ulm2  24980  lgsqrmodndvds  25937  2lgsoddprm  26000  ax5seglem5  26727  wlkdlem4  27475  clwwlknonwwlknonb  27891  3wlkdlem4  27947  spanunsni  29362  nonbooli  29434  nmopun  29797  lncnopbd  29820  pjnmopi  29931  sumdmdlem  30201  disjun0  30358  rnmposs  30437  esumpcvgval  31447  bnj545  32277  bnj900  32311  bnj1498  32443  nummin  32474  soseq  33209  btwnconn1lem7  33667  ivthALT  33796  topfneec  33816  bj-snglss  34406  bj-elpwg  34469  bj-ideqg1ALT  34580  bj-imdiridlem  34600  mptsnunlem  34755  icoreresf  34769  lindsenlbs  35052  matunitlindf  35055  poimirlem14  35071  poimirlem22  35079  poimirlem26  35083  poimirlem29  35086  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  fdc  35183  ismtyres  35246  isdrngo3  35397  lshpset2N  36415  3dimlem1  36754  3dim3  36765  cdleme31fv2  37689  fsuppind  39456  isnumbasgrplem3  40049  pm13.13b  41112  ax6e2ndeqALT  41637  sineq0ALT  41643  elrnmpt1sf  41816  requad1  44140  nn0sumshdiglemB  45034