Theorem biimparc 484

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

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

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 401

This theorem is referenced by:  biantr  817  eqtr3  2785  spc2ed  3561  elrab3t  3650  difprsnss  4768  elpw2g  5305  ideqg  5839  elrnmpt1s  5951  elrnmptg  5953  tz6.12-1  6906  eqfnfv2  7028  fmpt  7107  elunirn  7251  sucexeloni  7809  f1iun  7942  soseq  8156  tposfo2  8246  tposf12  8248  dom2lem  8990  ssnnfi  9155  ssfi  9158  enfii  9171  ac6sfi  9245  unfilem1  9266  pwfir  9277  nelaneq  9565  inf3lem2  9599  infdiffi  9628  dfac5lem5  10112  dfac2b  10115  dfac12k  10132  cfslb2n  10253  enfin2i  10306  fin23lem19  10321  axdc2lem  10433  axdc3lem4  10438  winainflem  10679  indpi  10893  ltexnq  10961  ltbtwnnq  10964  ltexprlem6  11027  prlem936  11033  elreal2  11118  fimaxre3  12162  addmodlteq  13984  expnbnd  14270  opfi1uzind  14550  repswswrd  14823  cshwidxmod  14842  climcnds  15907  fprod2dlem  16036  fprodle  16052  unbenlem  16969  acsfn  17716  lsmcv  21246  maducoeval2  22778  bastop2  23132  neipeltop  23267  rnelfmlem  24090  isfcls  24147  tgphaus  24255  mbfi1fseqlem4  25858  ulm2  26526  lgsqrmodndvds  27495  2lgsoddprm  27558  ax5seglem5  29261  wlkdlem4  30011  clwwlknonwwlknonb  30435  3wlkdlem4  30491  spanunsni  31909  nonbooli  31981  nmopun  32344  lncnopbd  32367  pjnmopi  32478  sumdmdlem  32748  disjun0  32918  rnmposs  32996  elrgspnlem2  33541  elrgspnlem3  33542  esumpcvgval  34446  bnj545  35261  bnj900  35295  bnj1498  35427  nummin  35462  fineqvac  35507  fineqvnttrclselem1  35512  noinfepfnregs  35523  wevgblacfn  35573  btwnconn1lem7  36563  ivthALT  36824  topfneec  36844  bj-elabd2ALT  37539  bj-snglss  37584  bj-elpwg  37666  bj-ideqg1ALT  37787  bj-imdiridlem  37807  mptsnunlem  37962  icoreresf  37976  lindsenlbs  38244  matunitlindf  38247  poimirlem14  38263  poimirlem22  38271  poimirlem26  38275  poimirlem29  38278  ovoliunnfl  38291  voliunnfl  38293  volsupnfl  38294  fdc  38374  ismtyres  38437  isdrngo3  38588  lshpset2N  39871  3dimlem1  40210  3dim3  40221  cdleme31fv2  41145  fsuppind  43302  isnumbasgrplem3  43812  pm13.13b  45098  ax6e2ndeqALT  45619  sineq0ALT  45625  elrnmpt1sf  45887  requad1  48364  clnbgrel  48570  nn0sumshdiglemB  49377  ipolubdm  49742  ipoglbdm  49745