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  2751  spc2ed  3553  elrab3t  3643  difprsnss  4748  elpw2g  5268  ideqg  5788  elrnmpt1s  5895  elrnmptg  5897  tz6.12-1  6839  eqfnfv2  6959  fmpt  7037  elunirn  7179  sucexeloni  7736  f1iun  7870  soseq  8083  tposfo2  8173  tposf12  8175  dom2lem  8908  ssnnfi  9073  ssfi  9076  enfii  9089  ac6sfi  9162  unfilem1  9183  pwfir  9195  inf3lem2  9513  infdiffi  9542  dfac5lem5  10009  dfac2b  10013  dfac12k  10030  cfslb2n  10150  enfin2i  10203  fin23lem19  10218  axdc2lem  10330  axdc3lem4  10335  winainflem  10575  indpi  10789  ltexnq  10857  ltbtwnnq  10860  ltexprlem6  10923  prlem936  10929  elreal2  11014  fimaxre3  12059  addmodlteq  13841  expnbnd  14127  opfi1uzind  14406  repswswrd  14678  cshwidxmod  14697  climcnds  15745  fprod2dlem  15874  fprodle  15890  unbenlem  16807  acsfn  17552  lsmcv  21032  maducoeval2  22509  bastop2  22863  neipeltop  22998  rnelfmlem  23821  isfcls  23878  tgphaus  23986  mbfi1fseqlem4  25600  ulm2  26275  lgsqrmodndvds  27245  2lgsoddprm  27308  ax5seglem5  28865  wlkdlem4  29616  clwwlknonwwlknonb  30037  3wlkdlem4  30093  spanunsni  31510  nonbooli  31582  nmopun  31945  lncnopbd  31968  pjnmopi  32079  sumdmdlem  32349  disjun0  32527  rnmposs  32608  elrgspnlem2  33178  elrgspnlem3  33179  esumpcvgval  34059  bnj545  34875  bnj900  34909  bnj1498  35041  nummin  35071  fineqvac  35085  fineqvnttrclselem1  35087  wevgblacfn  35099  btwnconn1lem7  36084  ivthALT  36326  topfneec  36346  bj-elabd2ALT  36916  bj-snglss  36961  bj-elpwg  37043  bj-ideqg1ALT  37156  bj-imdiridlem  37176  mptsnunlem  37329  icoreresf  37343  lindsenlbs  37612  matunitlindf  37615  poimirlem14  37631  poimirlem22  37639  poimirlem26  37643  poimirlem29  37646  ovoliunnfl  37659  voliunnfl  37661  volsupnfl  37662  fdc  37742  ismtyres  37805  isdrngo3  37956  lshpset2N  39115  3dimlem1  39454  3dim3  39465  cdleme31fv2  40389  fsuppind  42580  isnumbasgrplem3  43095  pm13.13b  44398  ax6e2ndeqALT  44920  sineq0ALT  44926  elrnmpt1sf  45183  requad1  47620  clnbgrel  47826  nn0sumshdiglemB  48619  ipolubdm  48985  ipoglbdm  48988