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  3353  reuanid  3354  eueq3  3658  reu6  3673  reuan  3835  ifan  4521  dfopif  4814  notzfaus  5300  reusv2lem5  5339  dmopab2rex  5866  elpredg  6273  fvopab3g  6936  riota1a  7339  dfom2  7812  suppssr  8138  mpocurryd  8212  boxcutc  8882  funisfsupp  9273  dfac3  10034  eluz2  12785  elixx3g  13302  elfz2  13459  zmodid2  13849  shftfib  15025  dvdsssfz1  16278  modremain  16368  sadadd2lem2  16410  smumullem  16452  tltnle  18377  issubg  19093  resgrpisgrp  19114  sscntz  19292  pgrpsubgsymgbi  19374  qusecsub  19801  isrnghm  20412  rnghmval2  20415  issubrng  20515  issubrg  20539  lindsmm  21818  mdetunilem8  22594  mdetunilem9  22595  cmpsub  23375  txcnmpt  23599  hausdiag  23620  fbfinnfr  23816  elfilss  23851  fixufil  23897  ibladdlem  25797  iblabslem  25805  lenlts  27730  cusgruvtxb  29505  usgr0edg0rusgr  29659  rgrusgrprc  29673  rusgrnumwwlkslem  30055  eclclwwlkn1  30160  eupth2lem1  30303  pjimai  32262  chrelati  32450  metidv  34052  satfv1lem  35560  dmopab3rexdif  35603  copsex2b  37470  curf  37933  unccur  37938  cnambfre  38003  itg2addnclem2  38007  ibladdnclem  38011  iblabsnclem  38018  prjsprellsp  43058  expdiophlem1  43467  rfovcnvf1od  44449  fsovrfovd  44454  ntrneiel2  44531  odd2np1ALTV  48162  clnbupgrel  48322  dfvopnbgr2  48341  vopnbgrelself  48343  uzlidlring  48723  islindeps  48941  elbigo2  49040