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  2616  moanim  2617  euan  2618  euanv  2621  ralanid  3081  rexanid  3082  r19.29  3096  rmoanid  3357  reuanid  3358  eueq3  3666  reu6  3681  reuan  3843  ifan  4528  dfopif  4821  notzfaus  5303  reusv2lem5  5342  dmopab2rex  5861  elpredg  6267  fvopab3g  6930  riota1a  7331  dfom2  7804  suppssr  8131  mpocurryd  8205  boxcutc  8871  funisfsupp  9258  dfac3  10019  eluz2  12744  elixx3g  13260  elfz2  13416  zmodid2  13805  shftfib  14981  dvdsssfz1  16231  modremain  16321  sadadd2lem2  16363  smumullem  16405  tltnle  18328  issubg  19041  resgrpisgrp  19062  sscntz  19240  pgrpsubgsymgbi  19322  qusecsub  19749  isrnghm  20361  rnghmval2  20364  issubrng  20464  issubrg  20488  lindsmm  21767  mdetunilem8  22535  mdetunilem9  22536  cmpsub  23316  txcnmpt  23540  hausdiag  23561  fbfinnfr  23757  elfilss  23792  fixufil  23838  ibladdlem  25749  iblabslem  25757  slenlt  27692  cusgruvtxb  29402  usgr0edg0rusgr  29556  rgrusgrprc  29570  rusgrnumwwlkslem  29952  eclclwwlkn1  30057  eupth2lem1  30200  pjimai  32158  chrelati  32346  bian1d  32437  metidv  33926  satfv1lem  35427  dmopab3rexdif  35470  copsex2b  37205  curf  37659  unccur  37664  cnambfre  37729  itg2addnclem2  37733  ibladdnclem  37737  iblabsnclem  37744  prjsprellsp  42730  expdiophlem1  43139  rfovcnvf1od  44122  fsovrfovd  44127  ntrneiel2  44204  odd2np1ALTV  47799  clnbupgrel  47959  dfvopnbgr2  47978  vopnbgrelself  47980  uzlidlring  48360  islindeps  48579  elbigo2  48678