Theorem ibar 528

Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)

Assertion

Ref	Expression
ibar	⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		iba 527	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
2	1	biancomd 463	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:  biantrurd  532  baib  535  baibd  539  bianabs  541  pm5.42  543  anclb  545  anabs5  663  annotanannot  834  pm5.33  835  pclem6  1027  moanimv  2617  moanim  2618  euan  2619  euanv  2622  ralanid  3083  rexanid  3084  r19.29  3101  rmoanid  3374  reuanid  3375  eueq3  3701  reu6  3716  reuan  3878  ifan  4561  dfopif  4852  notzfaus  5345  reusv2lem5  5384  dmopab2rex  5910  elpredg  6317  fvopab3g  6992  riota1a  7393  dfom2  7872  suppssr  8203  mpocurryd  8277  boxcutc  8964  funisfsupp  9390  dfac3  10144  eluz2  12867  elixx3g  13383  elfz2  13537  zmodid2  13922  shftfib  15094  dvdsssfz1  16338  modremain  16428  sadadd2lem2  16470  smumullem  16512  tltnle  18441  issubg  19118  resgrpisgrp  19139  sscntz  19318  pgrpsubgsymgbi  19399  qusecsub  19826  isrnghm  20414  rnghmval2  20417  issubrng  20520  issubrg  20544  lindsmm  21815  mdetunilem8  22592  mdetunilem9  22593  cmpsub  23373  txcnmpt  23597  hausdiag  23618  fbfinnfr  23814  elfilss  23849  fixufil  23895  ibladdlem  25810  iblabslem  25818  slenlt  27752  cusgruvtxb  29386  usgr0edg0rusgr  29540  rgrusgrprc  29554  rusgrnumwwlkslem  29936  eclclwwlkn1  30041  eupth2lem1  30184  pjimai  32142  chrelati  32330  bian1d  32422  metidv  33832  satfv1lem  35308  dmopab3rexdif  35351  copsex2b  37082  curf  37546  unccur  37551  cnambfre  37616  itg2addnclem2  37620  ibladdnclem  37624  iblabsnclem  37631  prjsprellsp  42566  expdiophlem1  42978  rfovcnvf1od  43962  fsovrfovd  43967  ntrneiel2  44044  odd2np1ALTV  47607  clnbupgrel  47767  dfvopnbgr2  47785  vopnbgrelself  47787  uzlidlring  48097  islindeps  48316  elbigo2  48419