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  664  annotanannot  835  pm5.33  836  pclem6  1028  moanimv  2620  moanim  2621  euan  2622  euanv  2625  ralanid  3086  rexanid  3087  r19.29  3101  rmoanid  3362  reuanid  3363  eueq3  3671  reu6  3686  reuan  3848  ifan  4535  dfopif  4828  notzfaus  5310  reusv2lem5  5349  dmopab2rex  5874  elpredg  6281  fvopab3g  6944  riota1a  7347  dfom2  7820  suppssr  8147  mpocurryd  8221  boxcutc  8891  funisfsupp  9282  dfac3  10043  eluz2  12769  elixx3g  13286  elfz2  13442  zmodid2  13831  shftfib  15007  dvdsssfz1  16257  modremain  16347  sadadd2lem2  16389  smumullem  16431  tltnle  18355  issubg  19068  resgrpisgrp  19089  sscntz  19267  pgrpsubgsymgbi  19349  qusecsub  19776  isrnghm  20389  rnghmval2  20392  issubrng  20492  issubrg  20516  lindsmm  21795  mdetunilem8  22575  mdetunilem9  22576  cmpsub  23356  txcnmpt  23580  hausdiag  23601  fbfinnfr  23797  elfilss  23832  fixufil  23878  ibladdlem  25789  iblabslem  25797  lenlts  27732  cusgruvtxb  29507  usgr0edg0rusgr  29661  rgrusgrprc  29675  rusgrnumwwlkslem  30057  eclclwwlkn1  30162  eupth2lem1  30305  pjimai  32263  chrelati  32451  metidv  34069  satfv1lem  35575  dmopab3rexdif  35618  copsex2b  37392  curf  37846  unccur  37851  cnambfre  37916  itg2addnclem2  37920  ibladdnclem  37924  iblabsnclem  37931  prjsprellsp  42966  expdiophlem1  43375  rfovcnvf1od  44357  fsovrfovd  44362  ntrneiel2  44439  odd2np1ALTV  48031  clnbupgrel  48191  dfvopnbgr2  48210  vopnbgrelself  48212  uzlidlring  48592  islindeps  48810  elbigo2  48909