Theorem ibar 527

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

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

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 395

This theorem is referenced by:  biantrurd  531  baib  534  baibd  538  bianabs  540  pm5.42  542  anclb  544  anabs5  661  annotanannot  833  pm5.33  834  pclem6  1023  moanimv  2608  moanim  2609  euan  2610  euanv  2613  ralanid  3085  rexanid  3086  r19.29  3104  rmoanid  3375  reuanid  3376  eueq3  3705  reu6  3720  reuan  3889  ifan  4577  dfopif  4869  notzfaus  5358  reusv2lem5  5397  dmopab2rex  5915  elpredg  6317  fvopab3g  6994  riota1a  7393  dfom2  7868  suppssr  8200  mpocurryd  8274  boxcutc  8960  funisfsupp  9402  dfac3  10155  eluz2  12872  elixx3g  13383  elfz2  13537  zmodid2  13911  shftfib  15070  dvdsssfz1  16313  modremain  16403  sadadd2lem2  16443  smumullem  16485  tltnle  18440  issubg  19114  resgrpisgrp  19135  sscntz  19314  pgrpsubgsymgbi  19400  qusecsub  19827  isrnghm  20417  rnghmval2  20420  issubrng  20523  issubrg  20549  lindsmm  21820  mdetunilem8  22607  mdetunilem9  22608  cmpsub  23390  txcnmpt  23614  hausdiag  23635  fbfinnfr  23831  elfilss  23866  fixufil  23912  ibladdlem  25835  iblabslem  25843  slenlt  27777  cusgruvtxb  29353  usgr0edg0rusgr  29507  rgrusgrprc  29521  rusgrnumwwlkslem  29898  eclclwwlkn1  30003  eupth2lem1  30146  pjimai  32104  chrelati  32292  bian1d  32380  metidv  33718  satfv1lem  35201  dmopab3rexdif  35244  copsex2b  36858  curf  37310  unccur  37315  cnambfre  37380  itg2addnclem2  37384  ibladdnclem  37388  iblabsnclem  37395  prjsprellsp  42299  expdiophlem1  42714  rfovcnvf1od  43706  fsovrfovd  43711  ntrneiel2  43788  odd2np1ALTV  47280  clnbupgrel  47439  dfvopnbgr2  47454  vopnbgrelself  47456  uzlidlring  47646  islindeps  47870  elbigo2  47974