Theorem ibar 528

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  biantrurd  532  baib  535  baibd  539  bianabs  541  pm5.42  543  anclb  545  anabs5  664  annotanannot  835  pm5.33  836  pclem6  1028  moanimv  2619  moanim  2620  euan  2621  euanv  2624  ralanid  3085  rexanid  3086  r19.29  3100  rmoanid  3352  reuanid  3353  eueq3  3657  reu6  3672  reuan  3834  ifan  4520  dfopif  4813  notzfaus  5305  reusv2lem5  5344  dmopab2rex  5872  elpredg  6279  fvopab3g  6942  riota1a  7346  dfom2  7819  suppssr  8145  mpocurryd  8219  boxcutc  8889  funisfsupp  9280  dfac3  10043  eluz2  12794  elixx3g  13311  elfz2  13468  zmodid2  13858  shftfib  15034  dvdsssfz1  16287  modremain  16377  sadadd2lem2  16419  smumullem  16461  tltnle  18386  issubg  19102  resgrpisgrp  19123  sscntz  19301  pgrpsubgsymgbi  19383  qusecsub  19810  isrnghm  20421  rnghmval2  20424  issubrng  20524  issubrg  20548  lindsmm  21808  mdetunilem8  22584  mdetunilem9  22585  cmpsub  23365  txcnmpt  23589  hausdiag  23610  fbfinnfr  23806  elfilss  23841  fixufil  23887  ibladdlem  25787  iblabslem  25795  lenlts  27716  cusgruvtxb  29491  usgr0edg0rusgr  29644  rgrusgrprc  29658  rusgrnumwwlkslem  30040  eclclwwlkn1  30145  eupth2lem1  30288  pjimai  32247  chrelati  32435  metidv  34036  satfv1lem  35544  dmopab3rexdif  35587  copsex2b  37454  curf  37919  unccur  37924  cnambfre  37989  itg2addnclem2  37993  ibladdnclem  37997  iblabsnclem  38004  prjsprellsp  43044  expdiophlem1  43449  rfovcnvf1od  44431  fsovrfovd  44436  ntrneiel2  44513  odd2np1ALTV  48150  clnbupgrel  48310  dfvopnbgr2  48329  vopnbgrelself  48331  uzlidlring  48711  islindeps  48929  elbigo2  49028