Theorem biimparc 485

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biantr  818  eqtr3  2788  spc2ed  3563  elrab3t  3652  difprsnss  4772  elpw2g  5309  ideqg  5842  elrnmpt1s  5954  elrnmptg  5956  tz6.12-1  6911  eqfnfv2  7033  fmpt  7112  elunirn  7256  sucexeloni  7817  f1iun  7950  soseq  8164  tposfo2  8254  tposf12  8256  dom2lem  8998  ssnnfi  9164  ssfi  9167  enfii  9180  ac6sfi  9254  unfilem1  9275  pwfir  9286  nelaneq  9574  inf3lem2  9608  infdiffi  9637  dfac5lem5  10130  dfac2b  10133  dfac12k  10150  cfslb2n  10270  enfin2i  10323  fin23lem19  10338  axdc2lem  10450  axdc3lem4  10455  winainflem  10696  indpi  10910  ltexnq  10978  ltbtwnnq  10981  ltexprlem6  11044  prlem936  11050  elreal2  11135  fimaxre3  12179  addmodlteq  14002  expnbnd  14288  opfi1uzind  14568  repswswrd  14847  cshwidxmod  14866  climcnds  15931  fprod2dlem  16060  fprodle  16076  unbenlem  16993  acsfn  17740  isdrng5  20891  lsmcv  21302  maducoeval2  22834  bastop2  23188  neipeltop  23323  rnelfmlem  24146  isfcls  24203  tgphaus  24311  mbfi1fseqlem4  25914  ulm2  26585  lgsqrmodndvds  27554  2lgsoddprm  27617  ax5seglem5  29320  wlkdlem4  30070  clwwlknonwwlknonb  30494  3wlkdlem4  30550  spanunsni  31968  nonbooli  32040  nmopun  32403  lncnopbd  32426  pjnmopi  32537  sumdmdlem  32807  disjun0  32977  rnmposs  33055  elrgspnlem2  33594  elrgspnlem3  33595  esumpcvgval  34499  bnj545  35315  bnj900  35349  bnj1498  35481  nummin  35509  fineqvac  35553  fineqvnttrclselem1  35558  noinfepfnregs  35569  wevgblacfn  35619  btwnconn1lem7  36606  ivthALT  36887  topfneec  36907  bj-elabd2ALT  37602  bj-snglss  37647  bj-elpwg  37729  bj-ideqg1ALT  37850  bj-imdiridlem  37870  mptsnunlem  38025  icoreresf  38039  lindsenlbs  38307  matunitlindf  38310  poimirlem14  38326  poimirlem22  38334  poimirlem26  38338  poimirlem29  38341  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  fdc  38437  ismtyres  38500  isdrngo3  38651  lshpset2N  39934  3dimlem1  40273  3dim3  40284  cdleme31fv2  41208  fsuppind  43363  isnumbasgrplem3  43873  pm13.13b  45159  ax6e2ndeqALT  45680  sineq0ALT  45686  elrnmpt1sf  45948  requad1  48428  clnbgrel  48634  nn0sumshdiglemB  49441  ipolubdm  49806  ipoglbdm  49809