Theorem ibar 529

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 528	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
2	1	biancomd 464	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  biantrurd  533  baib  536  baibd  540  bianabs  542  pm5.42  544  anclb  546  anabs5  661  annotanannot  833  pm5.33  834  pclem6  1024  moanimv  2619  moanim  2620  euan  2621  euanv  2624  ralanid  3098  rexanid  3099  r19.29  3117  rmoanid  3363  reuanid  3364  eueq3  3669  reu6  3684  reuan  3852  ifan  4539  dfopif  4827  notzfaus  5318  reusv2lem5  5357  dmopab2rex  5873  elpredg  6267  fvopab3g  6943  riota1a  7336  dfom2  7804  suppssr  8127  mpocurryd  8200  boxcutc  8879  funisfsupp  9310  dfac3  10057  eluz2  12769  elixx3g  13277  elfz2  13431  zmodid2  13804  shftfib  14957  dvdsssfz1  16200  modremain  16290  sadadd2lem2  16330  smumullem  16372  tltnle  18311  issubg  18928  resgrpisgrp  18949  sscntz  19106  pgrpsubgsymgbi  19190  issubrg  20222  lindsmm  21234  mdetunilem8  21968  mdetunilem9  21969  cmpsub  22751  txcnmpt  22975  hausdiag  22996  fbfinnfr  23192  elfilss  23227  fixufil  23273  ibladdlem  25184  iblabslem  25192  slenlt  27100  cusgruvtxb  28370  usgr0edg0rusgr  28523  rgrusgrprc  28537  rusgrnumwwlkslem  28914  eclclwwlkn1  29019  eupth2lem1  29162  pjimai  31118  chrelati  31306  metidv  32473  satfv1lem  33956  dmopab3rexdif  33999  copsex2b  35611  curf  36056  unccur  36061  cnambfre  36126  itg2addnclem2  36130  ibladdnclem  36134  iblabsnclem  36141  prjsprellsp  40935  expdiophlem1  41331  rfovcnvf1od  42266  fsovrfovd  42271  ntrneiel2  42348  odd2np1ALTV  45856  isrnghm  46180  rnghmval2  46183  uzlidlring  46217  islindeps  46524  elbigo2  46628