Theorem ibar 533

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  biantrurd  537  baib  540  baibd  544  bianabs  546  pm5.42  548  anclb  550  anabs5  669  annotanannot  840  pm5.33  841  pclem6  1033  moanimv  2623  moanim  2624  euan  2625  euanv  2628  ralanid  3088  rexanid  3089  r19.29  3103  rmoanid  3355  reuanid  3356  eueq3  3659  reu6  3674  reuan  3835  ifan  4515  dfopif  4808  notzfaus  5299  reusv2lem5  5338  dmopab2rex  5866  elpredg  6273  fvopab3g  6937  riota1a  7342  dfom2  7815  suppssr  8142  mpocurryd  8216  boxcutc  8886  funisfsupp  9277  dfac3  10041  eluz2  12792  elixx3g  13309  elfz2  13466  zmodid2  13856  shftfib  15032  dvdsssfz1  16285  modremain  16375  sadadd2lem2  16417  smumullem  16459  tltnle  18384  issubg  19100  resgrpisgrp  19121  sscntz  19299  pgrpsubgsymgbi  19381  qusecsub  19808  isrnghm  20419  rnghmval2  20422  issubrng  20526  issubrg  20550  lindsmm  21810  mdetunilem8  22609  mdetunilem9  22610  cmpsub  23390  txcnmpt  23614  hausdiag  23635  fbfinnfr  23831  elfilss  23866  fixufil  23912  ibladdlem  25812  iblabslem  25820  lenlts  27741  cusgruvtxb  29516  usgr0edg0rusgr  29669  rgrusgrprc  29683  rusgrnumwwlkslem  30065  eclclwwlkn1  30170  eupth2lem1  30313  pjimai  32272  chrelati  32460  metidv  34083  satfv1lem  35597  dmopab3rexdif  35640  copsex2b  37507  curf  37972  unccur  37977  cnambfre  38042  itg2addnclem2  38046  ibladdnclem  38050  iblabsnclem  38057  prjsprellsp  43068  expdiophlem1  43473  rfovcnvf1od  44455  fsovrfovd  44460  ntrneiel2  44537  odd2np1ALTV  48172  clnbupgrel  48332  dfvopnbgr2  48351  vopnbgrelself  48353  uzlidlring  48733  islindeps  48951  elbigo2  49050