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  2619  moanim  2620  euan  2621  euanv  2624  ralanid  3085  rexanid  3086  r19.29  3102  rmoanid  3374  reuanid  3375  eueq3  3699  reu6  3714  reuan  3876  ifan  4559  dfopif  4851  notzfaus  5338  reusv2lem5  5377  dmopab2rex  5902  elpredg  6309  fvopab3g  6986  riota1a  7389  dfom2  7868  suppssr  8199  mpocurryd  8273  boxcutc  8960  funisfsupp  9384  dfac3  10140  eluz2  12863  elixx3g  13380  elfz2  13536  zmodid2  13921  shftfib  15096  dvdsssfz1  16342  modremain  16432  sadadd2lem2  16474  smumullem  16516  tltnle  18437  issubg  19114  resgrpisgrp  19135  sscntz  19314  pgrpsubgsymgbi  19394  qusecsub  19821  isrnghm  20406  rnghmval2  20409  issubrng  20512  issubrg  20536  lindsmm  21793  mdetunilem8  22562  mdetunilem9  22563  cmpsub  23343  txcnmpt  23567  hausdiag  23588  fbfinnfr  23784  elfilss  23819  fixufil  23865  ibladdlem  25778  iblabslem  25786  slenlt  27721  cusgruvtxb  29406  usgr0edg0rusgr  29560  rgrusgrprc  29574  rusgrnumwwlkslem  29956  eclclwwlkn1  30061  eupth2lem1  30204  pjimai  32162  chrelati  32350  bian1d  32442  metidv  33928  satfv1lem  35389  dmopab3rexdif  35432  copsex2b  37163  curf  37627  unccur  37632  cnambfre  37697  itg2addnclem2  37701  ibladdnclem  37705  iblabsnclem  37712  prjsprellsp  42609  expdiophlem1  43020  rfovcnvf1od  44003  fsovrfovd  44008  ntrneiel2  44085  odd2np1ALTV  47668  clnbupgrel  47828  dfvopnbgr2  47846  vopnbgrelself  47848  uzlidlring  48190  islindeps  48409  elbigo2  48512