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  662  annotanannot  834  pm5.33  835  pclem6  1026  moanimv  2622  moanim  2623  euan  2624  euanv  2627  ralanid  3101  rexanid  3102  r19.29  3120  rmoanid  3398  reuanid  3399  eueq3  3733  reu6  3748  reuan  3918  ifan  4601  dfopif  4894  notzfaus  5381  reusv2lem5  5420  dmopab2rex  5942  elpredg  6346  fvopab3g  7024  riota1a  7427  dfom2  7905  suppssr  8236  mpocurryd  8310  boxcutc  8999  funisfsupp  9437  dfac3  10190  eluz2  12909  elixx3g  13420  elfz2  13574  zmodid2  13950  shftfib  15121  dvdsssfz1  16366  modremain  16456  sadadd2lem2  16496  smumullem  16538  tltnle  18492  issubg  19166  resgrpisgrp  19187  sscntz  19366  pgrpsubgsymgbi  19450  qusecsub  19877  isrnghm  20467  rnghmval2  20470  issubrng  20573  issubrg  20599  lindsmm  21871  mdetunilem8  22646  mdetunilem9  22647  cmpsub  23429  txcnmpt  23653  hausdiag  23674  fbfinnfr  23870  elfilss  23905  fixufil  23951  ibladdlem  25875  iblabslem  25883  slenlt  27815  cusgruvtxb  29457  usgr0edg0rusgr  29611  rgrusgrprc  29625  rusgrnumwwlkslem  30002  eclclwwlkn1  30107  eupth2lem1  30250  pjimai  32208  chrelati  32396  bian1d  32484  metidv  33838  satfv1lem  35330  dmopab3rexdif  35373  copsex2b  37106  curf  37558  unccur  37563  cnambfre  37628  itg2addnclem2  37632  ibladdnclem  37636  iblabsnclem  37643  prjsprellsp  42566  expdiophlem1  42978  rfovcnvf1od  43966  fsovrfovd  43971  ntrneiel2  44048  odd2np1ALTV  47548  clnbupgrel  47707  dfvopnbgr2  47725  vopnbgrelself  47727  uzlidlring  47958  islindeps  48182  elbigo2  48286