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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  biantr  802  eqtr3  2764  spc2ed  3530  elrab3t  3616  difprsnss  4729  elpw2g  5263  ideqg  5749  elrnmpt1s  5855  elrnmptg  5857  eqfnfv2  6892  fmpt  6966  elunirn  7106  f1iun  7760  tposfo2  8036  tposf12  8038  dom2lem  8735  ssnnfi  8914  ssnnfiOLD  8915  ssfi  8918  pwfir  8921  enfii  8932  enfiiOLD  8968  ac6sfi  8988  unfilem1  9008  inf3lem2  9317  infdiffi  9346  dfac5lem5  9814  dfac2b  9817  dfac12k  9834  cfslb2n  9955  enfin2i  10008  fin23lem19  10023  axdc2lem  10135  axdc3lem4  10140  winainflem  10380  indpi  10594  ltexnq  10662  ltbtwnnq  10665  ltexprlem6  10728  prlem936  10734  elreal2  10819  fimaxre3  11851  addmodlteq  13594  expnbnd  13875  opfi1uzind  14143  repswswrd  14425  cshwidxmod  14444  climcnds  15491  fprod2dlem  15618  fprodle  15634  unbenlem  16537  acsfn  17285  lsmcv  20318  maducoeval2  21697  bastop2  22052  neipeltop  22188  rnelfmlem  23011  isfcls  23068  tgphaus  23176  mbfi1fseqlem4  24788  ulm2  25449  lgsqrmodndvds  26406  2lgsoddprm  26469  ax5seglem5  27204  wlkdlem4  27955  clwwlknonwwlknonb  28371  3wlkdlem4  28427  spanunsni  29842  nonbooli  29914  nmopun  30277  lncnopbd  30300  pjnmopi  30411  sumdmdlem  30681  disjun0  30835  rnmposs  30913  esumpcvgval  31946  bnj545  32775  bnj900  32809  bnj1498  32941  nummin  32963  fineqvac  32966  soseq  33730  btwnconn1lem7  34322  ivthALT  34451  topfneec  34471  bj-elabd2ALT  35040  bj-snglss  35087  bj-elpwg  35152  bj-ideqg1ALT  35263  bj-imdiridlem  35283  mptsnunlem  35436  icoreresf  35450  lindsenlbs  35699  matunitlindf  35702  poimirlem14  35718  poimirlem22  35726  poimirlem26  35730  poimirlem29  35733  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  fdc  35830  ismtyres  35893  isdrngo3  36044  lshpset2N  37060  3dimlem1  37399  3dim3  37410  cdleme31fv2  38334  fsuppind  40202  isnumbasgrplem3  40846  pm13.13b  41915  ax6e2ndeqALT  42440  sineq0ALT  42446  elrnmpt1sf  42616  requad1  44962  nn0sumshdiglemB  45854  ipolubdm  46161  ipoglbdm  46164