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  835  pm5.33  836  pclem6  1027  moanimv  2617  moanim  2618  euan  2619  euanv  2622  ralanid  3093  rexanid  3094  r19.29  3112  rmoanid  3388  reuanid  3389  eueq3  3720  reu6  3735  reuan  3905  ifan  4584  dfopif  4875  notzfaus  5369  reusv2lem5  5408  dmopab2rex  5931  elpredg  6337  fvopab3g  7011  riota1a  7410  dfom2  7889  suppssr  8219  mpocurryd  8293  boxcutc  8980  funisfsupp  9405  dfac3  10159  eluz2  12882  elixx3g  13397  elfz2  13551  zmodid2  13936  shftfib  15108  dvdsssfz1  16352  modremain  16442  sadadd2lem2  16484  smumullem  16526  tltnle  18480  issubg  19157  resgrpisgrp  19178  sscntz  19357  pgrpsubgsymgbi  19441  qusecsub  19868  isrnghm  20458  rnghmval2  20461  issubrng  20564  issubrg  20588  lindsmm  21866  mdetunilem8  22641  mdetunilem9  22642  cmpsub  23424  txcnmpt  23648  hausdiag  23669  fbfinnfr  23865  elfilss  23900  fixufil  23946  ibladdlem  25870  iblabslem  25878  slenlt  27812  cusgruvtxb  29454  usgr0edg0rusgr  29608  rgrusgrprc  29622  rusgrnumwwlkslem  29999  eclclwwlkn1  30104  eupth2lem1  30247  pjimai  32205  chrelati  32393  bian1d  32484  metidv  33853  satfv1lem  35347  dmopab3rexdif  35390  copsex2b  37123  curf  37585  unccur  37590  cnambfre  37655  itg2addnclem2  37659  ibladdnclem  37663  iblabsnclem  37670  prjsprellsp  42598  expdiophlem1  43010  rfovcnvf1od  43994  fsovrfovd  43999  ntrneiel2  44076  odd2np1ALTV  47599  clnbupgrel  47759  dfvopnbgr2  47777  vopnbgrelself  47779  uzlidlring  48079  islindeps  48299  elbigo2  48402