Theorem ibar 531

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  biantrurd  535  baib  538  baibd  542  bianabs  544  pm5.42  546  anclb  548  anabs5  661  annotanannot  832  pm5.33  833  pclem6  1022  moanimv  2700  moanim  2701  euan  2702  euanv  2705  ralanid  3168  rexanid  3252  eueq3  3702  reu6  3717  reuan  3880  ifan  4518  dfopif  4794  notzfaus  5255  reusv2lem5  5295  dmopab2rex  5781  fvopab3g  6758  riota1a  7130  dfom2  7576  suppssr  7855  mpocurryd  7929  boxcutc  8499  funisfsupp  8832  dfac3  9541  eluz2  12243  elixx3g  12745  elfz2  12893  zmodid2  13261  shftfib  14425  dvdsssfz1  15662  modremain  15753  sadadd2lem2  15793  smumullem  15835  issubg  18273  resgrpisgrp  18294  sscntz  18450  pgrpsubgsymgbi  18530  issubrg  19529  lindsmm  20966  mdetunilem8  21222  mdetunilem9  21223  cmpsub  22002  txcnmpt  22226  hausdiag  22247  fbfinnfr  22443  elfilss  22478  fixufil  22524  ibladdlem  24414  iblabslem  24422  cusgruvtxb  27198  usgr0edg0rusgr  27351  rgrusgrprc  27365  rusgrnumwwlkslem  27742  eclclwwlkn1  27848  eupth2lem1  27991  pjimai  29947  chrelati  30135  tltnle  30644  metidv  31127  satfv1lem  32604  dmopab3rexdif  32647  slenlt  33226  copsex2b  34426  curf  34864  unccur  34869  cnambfre  34934  itg2addnclem2  34938  ibladdnclem  34942  iblabsnclem  34949  prjsprellsp  39254  expdiophlem1  39611  rfovcnvf1od  40343  fsovrfovd  40348  ntrneiel2  40429  odd2np1ALTV  43832  isrnghm  44156  rnghmval2  44159  uzlidlring  44193  islindeps  44501  elbigo2  44605