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  2612  moanim  2613  euan  2614  euanv  2617  ralanid  3077  rexanid  3078  r19.29  3094  rmoanid  3364  reuanid  3365  eueq3  3682  reu6  3697  reuan  3859  ifan  4542  dfopif  4834  notzfaus  5318  reusv2lem5  5357  dmopab2rex  5881  elpredg  6288  fvopab3g  6963  riota1a  7366  dfom2  7844  suppssr  8174  mpocurryd  8248  boxcutc  8914  funisfsupp  9318  dfac3  10074  eluz2  12799  elixx3g  13319  elfz2  13475  zmodid2  13861  shftfib  15038  dvdsssfz1  16288  modremain  16378  sadadd2lem2  16420  smumullem  16462  tltnle  18381  issubg  19058  resgrpisgrp  19079  sscntz  19258  pgrpsubgsymgbi  19338  qusecsub  19765  isrnghm  20350  rnghmval2  20353  issubrng  20456  issubrg  20480  lindsmm  21737  mdetunilem8  22506  mdetunilem9  22507  cmpsub  23287  txcnmpt  23511  hausdiag  23532  fbfinnfr  23728  elfilss  23763  fixufil  23809  ibladdlem  25721  iblabslem  25729  slenlt  27664  cusgruvtxb  29349  usgr0edg0rusgr  29503  rgrusgrprc  29517  rusgrnumwwlkslem  29899  eclclwwlkn1  30004  eupth2lem1  30147  pjimai  32105  chrelati  32293  bian1d  32385  metidv  33882  satfv1lem  35349  dmopab3rexdif  35392  copsex2b  37128  curf  37592  unccur  37597  cnambfre  37662  itg2addnclem2  37666  ibladdnclem  37670  iblabsnclem  37677  prjsprellsp  42599  expdiophlem1  43010  rfovcnvf1od  43993  fsovrfovd  43998  ntrneiel2  44075  odd2np1ALTV  47675  clnbupgrel  47835  dfvopnbgr2  47853  vopnbgrelself  47855  uzlidlring  48223  islindeps  48442  elbigo2  48541