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  3084  rexanid  3085  r19.29  3099  rmoanid  3360  reuanid  3361  eueq3  3669  reu6  3684  reuan  3846  ifan  4533  dfopif  4826  notzfaus  5308  reusv2lem5  5347  dmopab2rex  5866  elpredg  6273  fvopab3g  6936  riota1a  7337  dfom2  7810  suppssr  8137  mpocurryd  8211  boxcutc  8879  funisfsupp  9270  dfac3  10031  eluz2  12757  elixx3g  13274  elfz2  13430  zmodid2  13819  shftfib  14995  dvdsssfz1  16245  modremain  16335  sadadd2lem2  16377  smumullem  16419  tltnle  18343  issubg  19056  resgrpisgrp  19077  sscntz  19255  pgrpsubgsymgbi  19337  qusecsub  19764  isrnghm  20377  rnghmval2  20380  issubrng  20480  issubrg  20504  lindsmm  21783  mdetunilem8  22563  mdetunilem9  22564  cmpsub  23344  txcnmpt  23568  hausdiag  23589  fbfinnfr  23785  elfilss  23820  fixufil  23866  ibladdlem  25777  iblabslem  25785  lenlts  27720  cusgruvtxb  29495  usgr0edg0rusgr  29649  rgrusgrprc  29663  rusgrnumwwlkslem  30045  eclclwwlkn1  30150  eupth2lem1  30293  pjimai  32251  chrelati  32439  bian1d  32530  metidv  34049  satfv1lem  35556  dmopab3rexdif  35599  copsex2b  37345  curf  37799  unccur  37804  cnambfre  37869  itg2addnclem2  37873  ibladdnclem  37877  iblabsnclem  37884  prjsprellsp  42854  expdiophlem1  43263  rfovcnvf1od  44245  fsovrfovd  44250  ntrneiel2  44327  odd2np1ALTV  47920  clnbupgrel  48080  dfvopnbgr2  48099  vopnbgrelself  48101  uzlidlring  48481  islindeps  48699  elbigo2  48798