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  3590  elrab3t  3680  difprsnss  4798  elpw2g  5340  ideqg  5846  elrnmpt1s  5951  elrnmptg  5953  tz6.12-1  6904  eqfnfv2  7022  fmpt  7097  elunirn  7237  sucexeloni  7784  f1iun  7917  soseq  8132  tposfo2  8221  tposf12  8223  dom2lem  8976  ssnnfi  9157  ssnnfiOLD  9158  ssfi  9161  pwfir  9164  enfii  9177  enfiiOLD  9252  ac6sfi  9275  unfilem1  9298  inf3lem2  9611  infdiffi  9640  dfac5lem5  10109  dfac2b  10112  dfac12k  10129  cfslb2n  10250  enfin2i  10303  fin23lem19  10318  axdc2lem  10430  axdc3lem4  10435  winainflem  10675  indpi  10889  ltexnq  10957  ltbtwnnq  10960  ltexprlem6  11023  prlem936  11029  elreal2  11114  fimaxre3  12147  addmodlteq  13898  expnbnd  14182  opfi1uzind  14449  repswswrd  14721  cshwidxmod  14740  climcnds  15784  fprod2dlem  15911  fprodle  15927  unbenlem  16828  acsfn  17590  lsmcv  20731  maducoeval2  22111  bastop2  22466  neipeltop  22602  rnelfmlem  23425  isfcls  23482  tgphaus  23590  mbfi1fseqlem4  25205  ulm2  25866  lgsqrmodndvds  26823  2lgsoddprm  26886  ax5seglem5  28158  wlkdlem4  28909  clwwlknonwwlknonb  29326  3wlkdlem4  29382  spanunsni  30797  nonbooli  30869  nmopun  31232  lncnopbd  31255  pjnmopi  31366  sumdmdlem  31636  disjun0  31792  rnmposs  31868  esumpcvgval  33007  bnj545  33837  bnj900  33871  bnj1498  34003  nummin  34025  fineqvac  34028  btwnconn1lem7  34996  ivthALT  35125  topfneec  35145  bj-elabd2ALT  35710  bj-snglss  35756  bj-elpwg  35838  bj-ideqg1ALT  35951  bj-imdiridlem  35971  mptsnunlem  36124  icoreresf  36138  lindsenlbs  36388  matunitlindf  36391  poimirlem14  36407  poimirlem22  36415  poimirlem26  36419  poimirlem29  36422  ovoliunnfl  36435  voliunnfl  36437  volsupnfl  36438  fdc  36519  ismtyres  36582  isdrngo3  36733  lshpset2N  37895  3dimlem1  38235  3dim3  38246  cdleme31fv2  39170  fsuppind  41051  isnumbasgrplem3  41718  pm13.13b  43038  ax6e2ndeqALT  43563  sineq0ALT  43569  elrnmpt1sf  43758  requad1  46163  nn0sumshdiglemB  47146  ipolubdm  47452  ipoglbdm  47455