Theorem biimparc 481

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  biantr  805  eqtr3  2759  spc2ed  3592  elrab3t  3682  difprsnss  4802  elpw2g  5344  ideqg  5850  elrnmpt1s  5955  elrnmptg  5957  tz6.12-1  6912  eqfnfv2  7031  fmpt  7107  elunirn  7247  sucexeloni  7794  f1iun  7927  soseq  8142  tposfo2  8231  tposf12  8233  dom2lem  8985  ssnnfi  9166  ssnnfiOLD  9167  ssfi  9170  pwfir  9173  enfii  9186  enfiiOLD  9261  ac6sfi  9284  unfilem1  9307  inf3lem2  9621  infdiffi  9650  dfac5lem5  10119  dfac2b  10122  dfac12k  10139  cfslb2n  10260  enfin2i  10313  fin23lem19  10328  axdc2lem  10440  axdc3lem4  10445  winainflem  10685  indpi  10899  ltexnq  10967  ltbtwnnq  10970  ltexprlem6  11033  prlem936  11039  elreal2  11124  fimaxre3  12157  addmodlteq  13908  expnbnd  14192  opfi1uzind  14459  repswswrd  14731  cshwidxmod  14750  climcnds  15794  fprod2dlem  15921  fprodle  15937  unbenlem  16838  acsfn  17600  lsmcv  20747  maducoeval2  22134  bastop2  22489  neipeltop  22625  rnelfmlem  23448  isfcls  23505  tgphaus  23613  mbfi1fseqlem4  25228  ulm2  25889  lgsqrmodndvds  26846  2lgsoddprm  26909  ax5seglem5  28181  wlkdlem4  28932  clwwlknonwwlknonb  29349  3wlkdlem4  29405  spanunsni  30820  nonbooli  30892  nmopun  31255  lncnopbd  31278  pjnmopi  31389  sumdmdlem  31659  disjun0  31814  rnmposs  31887  esumpcvgval  33065  bnj545  33895  bnj900  33929  bnj1498  34061  nummin  34083  fineqvac  34086  btwnconn1lem7  35054  ivthALT  35209  topfneec  35229  bj-elabd2ALT  35794  bj-snglss  35840  bj-elpwg  35922  bj-ideqg1ALT  36035  bj-imdiridlem  36055  mptsnunlem  36208  icoreresf  36222  lindsenlbs  36472  matunitlindf  36475  poimirlem14  36491  poimirlem22  36499  poimirlem26  36503  poimirlem29  36506  ovoliunnfl  36519  voliunnfl  36521  volsupnfl  36522  fdc  36602  ismtyres  36665  isdrngo3  36816  lshpset2N  37978  3dimlem1  38318  3dim3  38329  cdleme31fv2  39253  fsuppind  41160  isnumbasgrplem3  41833  pm13.13b  43153  ax6e2ndeqALT  43678  sineq0ALT  43684  elrnmpt1sf  43873  requad1  46277  nn0sumshdiglemB  47260  ipolubdm  47566  ipoglbdm  47569