Theorem biimparc 478

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

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

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 395

This theorem is referenced by:  biantr  802  eqtr3  2756  spc2ed  3590  elrab3t  3681  difprsnss  4801  elpw2g  5343  ideqg  5850  elrnmpt1s  5955  elrnmptg  5957  tz6.12-1  6913  eqfnfv2  7032  fmpt  7110  elunirn  7252  sucexeloni  7799  f1iun  7932  soseq  8147  tposfo2  8236  tposf12  8238  dom2lem  8990  ssnnfi  9171  ssnnfiOLD  9172  ssfi  9175  pwfir  9178  enfii  9191  enfiiOLD  9266  ac6sfi  9289  unfilem1  9312  inf3lem2  9626  infdiffi  9655  dfac5lem5  10124  dfac2b  10127  dfac12k  10144  cfslb2n  10265  enfin2i  10318  fin23lem19  10333  axdc2lem  10445  axdc3lem4  10450  winainflem  10690  indpi  10904  ltexnq  10972  ltbtwnnq  10975  ltexprlem6  11038  prlem936  11044  elreal2  11129  fimaxre3  12164  addmodlteq  13915  expnbnd  14199  opfi1uzind  14466  repswswrd  14738  cshwidxmod  14757  climcnds  15801  fprod2dlem  15928  fprodle  15944  unbenlem  16845  acsfn  17607  lsmcv  20899  maducoeval2  22362  bastop2  22717  neipeltop  22853  rnelfmlem  23676  isfcls  23733  tgphaus  23841  mbfi1fseqlem4  25468  ulm2  26133  lgsqrmodndvds  27092  2lgsoddprm  27155  ax5seglem5  28458  wlkdlem4  29209  clwwlknonwwlknonb  29626  3wlkdlem4  29682  spanunsni  31099  nonbooli  31171  nmopun  31534  lncnopbd  31557  pjnmopi  31668  sumdmdlem  31938  disjun0  32093  rnmposs  32166  esumpcvgval  33374  bnj545  34204  bnj900  34238  bnj1498  34370  nummin  34392  fineqvac  34395  btwnconn1lem7  35369  ivthALT  35523  topfneec  35543  bj-elabd2ALT  36108  bj-snglss  36154  bj-elpwg  36236  bj-ideqg1ALT  36349  bj-imdiridlem  36369  mptsnunlem  36522  icoreresf  36536  lindsenlbs  36786  matunitlindf  36789  poimirlem14  36805  poimirlem22  36813  poimirlem26  36817  poimirlem29  36820  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  fdc  36916  ismtyres  36979  isdrngo3  37130  lshpset2N  38292  3dimlem1  38632  3dim3  38643  cdleme31fv2  39567  fsuppind  41464  isnumbasgrplem3  42149  pm13.13b  43469  ax6e2ndeqALT  43994  sineq0ALT  44000  elrnmpt1sf  44186  requad1  46588  nn0sumshdiglemB  47393  ipolubdm  47699  ipoglbdm  47702