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  2759  spc2ed  3544  elrab3t  3634  difprsnss  4743  elpw2g  5270  ideqg  5800  elrnmpt1s  5908  elrnmptg  5910  tz6.12-1  6857  eqfnfv2  6978  fmpt  7056  elunirn  7199  sucexeloni  7756  f1iun  7890  soseq  8102  tposfo2  8192  tposf12  8194  dom2lem  8932  ssnnfi  9097  ssfi  9100  enfii  9113  ac6sfi  9187  unfilem1  9208  pwfir  9220  inf3lem2  9541  infdiffi  9570  dfac5lem5  10040  dfac2b  10044  dfac12k  10061  cfslb2n  10181  enfin2i  10234  fin23lem19  10249  axdc2lem  10361  axdc3lem4  10366  winainflem  10607  indpi  10821  ltexnq  10889  ltbtwnnq  10892  ltexprlem6  10955  prlem936  10961  elreal2  11046  fimaxre3  12093  addmodlteq  13899  expnbnd  14185  opfi1uzind  14464  repswswrd  14737  cshwidxmod  14756  climcnds  15807  fprod2dlem  15936  fprodle  15952  unbenlem  16870  acsfn  17616  lsmcv  21131  maducoeval2  22615  bastop2  22969  neipeltop  23104  rnelfmlem  23927  isfcls  23984  tgphaus  24092  mbfi1fseqlem4  25695  ulm2  26363  lgsqrmodndvds  27330  2lgsoddprm  27393  ax5seglem5  29016  wlkdlem4  29767  clwwlknonwwlknonb  30191  3wlkdlem4  30247  spanunsni  31665  nonbooli  31737  nmopun  32100  lncnopbd  32123  pjnmopi  32234  sumdmdlem  32504  disjun0  32680  rnmposs  32761  elrgspnlem2  33319  elrgspnlem3  33320  esumpcvgval  34238  bnj545  35053  bnj900  35087  bnj1498  35219  nummin  35252  fineqvac  35276  fineqvnttrclselem1  35281  noinfepfnregs  35292  wevgblacfn  35307  btwnconn1lem7  36291  ivthALT  36533  topfneec  36553  bj-elabd2ALT  37248  bj-snglss  37293  bj-elpwg  37375  bj-ideqg1ALT  37495  bj-imdiridlem  37515  mptsnunlem  37668  icoreresf  37682  lindsenlbs  37950  matunitlindf  37953  poimirlem14  37969  poimirlem22  37977  poimirlem26  37981  poimirlem29  37984  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  fdc  38080  ismtyres  38143  isdrngo3  38294  lshpset2N  39579  3dimlem1  39918  3dim3  39929  cdleme31fv2  40853  fsuppind  43037  isnumbasgrplem3  43551  pm13.13b  44853  ax6e2ndeqALT  45375  sineq0ALT  45381  elrnmpt1sf  45637  requad1  48110  clnbgrel  48316  nn0sumshdiglemB  49108  ipolubdm  49474  ipoglbdm  49477