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  660  annotanannot  832  pm5.33  833  pclem6  1023  moanimv  2622  moanim  2623  euan  2624  euanv  2627  ralanid  3095  rexanid  3184  eueq3  3647  reu6  3662  reuan  3830  ifan  4513  dfopifOLD  4802  notzfaus  5286  reusv2lem5  5326  dmopab2rex  5829  elpredg  6220  fvopab3g  6879  riota1a  7264  dfom2  7723  suppssr  8021  mpocurryd  8094  boxcutc  8738  funisfsupp  9142  dfac3  9886  eluz2  12597  elixx3g  13101  elfz2  13255  zmodid2  13628  shftfib  14792  dvdsssfz1  16036  modremain  16126  sadadd2lem2  16166  smumullem  16208  tltnle  18149  issubg  18764  resgrpisgrp  18785  sscntz  18941  pgrpsubgsymgbi  19025  issubrg  20033  lindsmm  21044  mdetunilem8  21777  mdetunilem9  21778  cmpsub  22560  txcnmpt  22784  hausdiag  22805  fbfinnfr  23001  elfilss  23036  fixufil  23082  ibladdlem  24993  iblabslem  25001  cusgruvtxb  27798  usgr0edg0rusgr  27951  rgrusgrprc  27965  rusgrnumwwlkslem  28343  eclclwwlkn1  28448  eupth2lem1  28591  pjimai  30547  chrelati  30735  metidv  31851  satfv1lem  33333  dmopab3rexdif  33376  slenlt  33964  copsex2b  35320  curf  35764  unccur  35769  cnambfre  35834  itg2addnclem2  35838  ibladdnclem  35842  iblabsnclem  35849  prjsprellsp  40457  expdiophlem1  40850  rfovcnvf1od  41619  fsovrfovd  41624  ntrneiel2  41703  odd2np1ALTV  45137  isrnghm  45461  rnghmval2  45464  uzlidlring  45498  islindeps  45805  elbigo2  45909