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  2615  moanim  2616  euan  2617  euanv  2620  ralanid  3095  rexanid  3096  r19.29  3114  rmoanid  3386  reuanid  3387  eueq3  3706  reu6  3721  reuan  3889  ifan  4580  dfopif  4869  notzfaus  5360  reusv2lem5  5399  dmopab2rex  5915  elpredg  6311  fvopab3g  6990  riota1a  7384  dfom2  7853  suppssr  8177  mpocurryd  8250  boxcutc  8931  funisfsupp  9363  dfac3  10112  eluz2  12824  elixx3g  13333  elfz2  13487  zmodid2  13860  shftfib  15015  dvdsssfz1  16257  modremain  16347  sadadd2lem2  16387  smumullem  16429  tltnle  18371  issubg  19000  resgrpisgrp  19021  sscntz  19184  pgrpsubgsymgbi  19270  qusecsub  19697  issubrg  20355  lindsmm  21374  mdetunilem8  22112  mdetunilem9  22113  cmpsub  22895  txcnmpt  23119  hausdiag  23140  fbfinnfr  23336  elfilss  23371  fixufil  23417  ibladdlem  25328  iblabslem  25336  slenlt  27244  cusgruvtxb  28668  usgr0edg0rusgr  28821  rgrusgrprc  28835  rusgrnumwwlkslem  29212  eclclwwlkn1  29317  eupth2lem1  29460  pjimai  31416  chrelati  31604  metidv  32860  satfv1lem  34341  dmopab3rexdif  34384  copsex2b  36009  curf  36454  unccur  36459  cnambfre  36524  itg2addnclem2  36528  ibladdnclem  36532  iblabsnclem  36539  prjsprellsp  41349  expdiophlem1  41745  rfovcnvf1od  42740  fsovrfovd  42745  ntrneiel2  42822  odd2np1ALTV  46328  isrnghm  46675  rnghmval2  46678  issubrng  46710  uzlidlring  46780  islindeps  47087  elbigo2  47191