Theorem ibar 530

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 529	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
2	1	biancomd 465	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

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

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 398

This theorem is referenced by:  biantrurd  534  baib  537  baibd  541  bianabs  543  pm5.42  545  anclb  547  anabs5  662  annotanannot  834  pm5.33  835  pclem6  1025  moanimv  2616  moanim  2617  euan  2618  euanv  2621  ralanid  3096  rexanid  3097  r19.29  3115  rmoanid  3387  reuanid  3388  eueq3  3708  reu6  3723  reuan  3891  ifan  4582  dfopif  4871  notzfaus  5362  reusv2lem5  5401  dmopab2rex  5918  elpredg  6315  fvopab3g  6994  riota1a  7388  dfom2  7857  suppssr  8181  mpocurryd  8254  boxcutc  8935  funisfsupp  9367  dfac3  10116  eluz2  12828  elixx3g  13337  elfz2  13491  zmodid2  13864  shftfib  15019  dvdsssfz1  16261  modremain  16351  sadadd2lem2  16391  smumullem  16433  tltnle  18375  issubg  19006  resgrpisgrp  19027  sscntz  19190  pgrpsubgsymgbi  19276  qusecsub  19703  issubrg  20319  lindsmm  21383  mdetunilem8  22121  mdetunilem9  22122  cmpsub  22904  txcnmpt  23128  hausdiag  23149  fbfinnfr  23345  elfilss  23380  fixufil  23426  ibladdlem  25337  iblabslem  25345  slenlt  27255  cusgruvtxb  28679  usgr0edg0rusgr  28832  rgrusgrprc  28846  rusgrnumwwlkslem  29223  eclclwwlkn1  29328  eupth2lem1  29471  pjimai  31429  chrelati  31617  metidv  32872  satfv1lem  34353  dmopab3rexdif  34396  copsex2b  36021  curf  36466  unccur  36471  cnambfre  36536  itg2addnclem2  36540  ibladdnclem  36544  iblabsnclem  36551  prjsprellsp  41353  expdiophlem1  41760  rfovcnvf1od  42755  fsovrfovd  42760  ntrneiel2  42837  odd2np1ALTV  46342  isrnghm  46690  rnghmval2  46693  issubrng  46726  uzlidlring  46827  islindeps  47134  elbigo2  47238