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  2614  moanim  2615  euan  2616  euanv  2619  ralanid  3080  rexanid  3081  r19.29  3095  rmoanid  3356  reuanid  3357  eueq3  3670  reu6  3685  reuan  3847  ifan  4529  dfopif  4822  notzfaus  5301  reusv2lem5  5340  dmopab2rex  5857  elpredg  6262  fvopab3g  6924  riota1a  7325  dfom2  7798  suppssr  8125  mpocurryd  8199  boxcutc  8865  funisfsupp  9251  dfac3  10012  eluz2  12738  elixx3g  13258  elfz2  13414  zmodid2  13803  shftfib  14979  dvdsssfz1  16229  modremain  16319  sadadd2lem2  16361  smumullem  16403  tltnle  18326  issubg  19039  resgrpisgrp  19060  sscntz  19239  pgrpsubgsymgbi  19321  qusecsub  19748  isrnghm  20360  rnghmval2  20363  issubrng  20463  issubrg  20487  lindsmm  21766  mdetunilem8  22535  mdetunilem9  22536  cmpsub  23316  txcnmpt  23540  hausdiag  23561  fbfinnfr  23757  elfilss  23792  fixufil  23838  ibladdlem  25749  iblabslem  25757  slenlt  27692  cusgruvtxb  29401  usgr0edg0rusgr  29555  rgrusgrprc  29569  rusgrnumwwlkslem  29948  eclclwwlkn1  30053  eupth2lem1  30196  pjimai  32154  chrelati  32342  bian1d  32433  metidv  33903  satfv1lem  35404  dmopab3rexdif  35447  copsex2b  37180  curf  37644  unccur  37649  cnambfre  37714  itg2addnclem2  37718  ibladdnclem  37722  iblabsnclem  37729  prjsprellsp  42650  expdiophlem1  43060  rfovcnvf1od  44043  fsovrfovd  44048  ntrneiel2  44125  odd2np1ALTV  47711  clnbupgrel  47871  dfvopnbgr2  47890  vopnbgrelself  47892  uzlidlring  48272  islindeps  48491  elbigo2  48590