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 252	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	imp 410	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  biantr  815  eqtr3  2783  spc2ed  3560  elrab3t  3649  difprsnss  4758  elpw2g  5288  ideqg  5821  elrnmpt1s  5933  elrnmptg  5935  tz6.12-1  6886  eqfnfv2  7008  fmpt  7087  elunirn  7231  sucexeloni  7788  f1iun  7921  soseq  8134  tposfo2  8224  tposf12  8226  dom2lem  8969  ssnnfi  9134  ssfi  9137  enfii  9150  ac6sfi  9224  unfilem1  9245  pwfir  9257  nelaneq  9547  inf3lem2  9581  infdiffi  9610  dfac5lem5  10080  dfac2b  10084  dfac12k  10101  cfslb2n  10222  enfin2i  10275  fin23lem19  10290  axdc2lem  10402  axdc3lem4  10407  winainflem  10648  indpi  10862  ltexnq  10930  ltbtwnnq  10933  ltexprlem6  10996  prlem936  11002  elreal2  11087  fimaxre3  12135  addmodlteq  13956  expnbnd  14242  opfi1uzind  14521  repswswrd  14794  cshwidxmod  14813  climcnds  15864  fprod2dlem  15993  fprodle  16009  unbenlem  16927  acsfn  17674  lsmcv  21191  maducoeval2  22680  bastop2  23034  neipeltop  23169  rnelfmlem  23992  isfcls  24049  tgphaus  24157  mbfi1fseqlem4  25760  ulm2  26425  lgsqrmodndvds  27394  2lgsoddprm  27457  ax5seglem5  29080  wlkdlem4  29830  clwwlknonwwlknonb  30254  3wlkdlem4  30310  spanunsni  31728  nonbooli  31800  nmopun  32163  lncnopbd  32186  pjnmopi  32297  sumdmdlem  32567  disjun0  32744  rnmposs  32825  elrgspnlem2  33385  elrgspnlem3  33386  esumpcvgval  34336  bnj545  35154  bnj900  35188  bnj1498  35320  nummin  35353  fineqvac  35376  fineqvnttrclselem1  35381  noinfepfnregs  35392  wevgblacfn  35418  btwnconn1lem7  36407  ivthALT  36659  topfneec  36679  bj-elabd2ALT  37374  bj-snglss  37419  bj-elpwg  37501  bj-ideqg1ALT  37621  bj-imdiridlem  37641  mptsnunlem  37796  icoreresf  37810  lindsenlbs  38078  matunitlindf  38081  poimirlem14  38097  poimirlem22  38105  poimirlem26  38109  poimirlem29  38112  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  fdc  38208  ismtyres  38271  isdrngo3  38422  lshpset2N  39707  3dimlem1  40046  3dim3  40057  cdleme31fv2  40981  fsuppind  43136  isnumbasgrplem3  43646  pm13.13b  44948  ax6e2ndeqALT  45470  sineq0ALT  45476  elrnmpt1sf  45731  requad1  48208  clnbgrel  48414  nn0sumshdiglemB  49206  ipolubdm  49572  ipoglbdm  49575