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  805  eqtr3  2758  spc2ed  3555  elrab3t  3645  difprsnss  4755  elpw2g  5278  ideqg  5800  elrnmpt1s  5908  elrnmptg  5910  tz6.12-1  6857  eqfnfv2  6977  fmpt  7055  elunirn  7197  sucexeloni  7754  f1iun  7888  soseq  8101  tposfo2  8191  tposf12  8193  dom2lem  8929  ssnnfi  9094  ssfi  9097  enfii  9110  ac6sfi  9184  unfilem1  9205  pwfir  9217  inf3lem2  9538  infdiffi  9567  dfac5lem5  10037  dfac2b  10041  dfac12k  10058  cfslb2n  10178  enfin2i  10231  fin23lem19  10246  axdc2lem  10358  axdc3lem4  10363  winainflem  10604  indpi  10818  ltexnq  10886  ltbtwnnq  10889  ltexprlem6  10952  prlem936  10958  elreal2  11043  fimaxre3  12088  addmodlteq  13869  expnbnd  14155  opfi1uzind  14434  repswswrd  14707  cshwidxmod  14726  climcnds  15774  fprod2dlem  15903  fprodle  15919  unbenlem  16836  acsfn  17582  lsmcv  21096  maducoeval2  22584  bastop2  22938  neipeltop  23073  rnelfmlem  23896  isfcls  23953  tgphaus  24061  mbfi1fseqlem4  25675  ulm2  26350  lgsqrmodndvds  27320  2lgsoddprm  27383  ax5seglem5  29006  wlkdlem4  29757  clwwlknonwwlknonb  30181  3wlkdlem4  30237  spanunsni  31654  nonbooli  31726  nmopun  32089  lncnopbd  32112  pjnmopi  32223  sumdmdlem  32493  disjun0  32670  rnmposs  32752  elrgspnlem2  33325  elrgspnlem3  33326  esumpcvgval  34235  bnj545  35051  bnj900  35085  bnj1498  35217  nummin  35249  fineqvac  35272  fineqvnttrclselem1  35277  noinfepfnregs  35288  wevgblacfn  35303  btwnconn1lem7  36287  ivthALT  36529  topfneec  36549  bj-elabd2ALT  37126  bj-snglss  37171  bj-elpwg  37253  bj-ideqg1ALT  37366  bj-imdiridlem  37386  mptsnunlem  37539  icoreresf  37553  lindsenlbs  37812  matunitlindf  37815  poimirlem14  37831  poimirlem22  37839  poimirlem26  37843  poimirlem29  37846  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  fdc  37942  ismtyres  38005  isdrngo3  38156  lshpset2N  39375  3dimlem1  39714  3dim3  39725  cdleme31fv2  40649  fsuppind  42829  isnumbasgrplem3  43343  pm13.13b  44645  ax6e2ndeqALT  45167  sineq0ALT  45173  elrnmpt1sf  45429  requad1  47864  clnbgrel  48070  nn0sumshdiglemB  48862  ipolubdm  49228  ipoglbdm  49231