Theorem ibar 538

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biantrurd  542  baib  545  baibd  549  bianabs  551  pm5.42  553  anclb  555  anabs5  676  annotanannot  848  pm5.33  849  pclem6  1043  moanimv  2646  moanim  2647  euan  2648  euanv  2651  ralanid  3112  rexanid  3113  r19.29  3127  rmoanid  3377  reuanid  3378  eueq3  3672  reu6  3687  reuan  3847  ifan  4539  dfopif  4833  notsep  5332  reusv2lem5  5371  dmopab2rex  5905  elpredg  6317  fvopab3g  6985  riota1a  7396  dfom2  7868  suppssr  8197  mpocurryd  8271  curf  8873  boxcutc  8952  funisfsupp  9341  dfac3  10128  eluz2  12897  elixx3g  13415  elfz2  13572  zmodid2  13964  shftfib  15149  dvdsssfz1  16414  modremain  16504  sadadd2lem2  16546  smumullem  16588  tltnle  18514  issubg  19255  resgrpisgrp  19277  sscntz  19459  pgrpsubgsymgbi  19541  qusecsub  19968  isrnghm  20588  rnghmval2  20591  issubrng  20715  issubrg  20739  lindsmm  22047  mdetunilem8  22847  mdetunilem9  22848  cmpsub  23631  txcnmpt  23856  hausdiag  23877  fbfinnfr  24073  elfilss  24108  fixufil  24154  ibladdlem  26054  iblabslem  26062  lenlts  27996  cusgruvtxb  29890  usgr0edg0rusgr  30043  rgrusgrprc  30057  rusgrnumwwlkslem  30448  eclclwwlkn1  30553  eupth2lem1  30706  pjimai  32665  chrelati  32853  metidv  34410  satfv1lem  35949  dmopab3rexdif  35992  copsex2b  37900  unccur  38365  cnambfre  38425  itg2addnclem2  38429  ibladdnclem  38433  iblabsnclem  38440  prjsprellsp  43465  expdiophlem1  43870  rfovcnvf1od  44852  fsovrfovd  44857  ntrneiel2  44934  odd2np1ALTV  48598  clnbupgrel  48758  dfvopnbgr2  48777  vopnbgrelself  48779  uzlidlring  49158  crngprmringidom  49264  islindeps  49391  elbigo2  49490  ralrals  50745  ralals  50751