Theorem ibar 537

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biantrurd  541  baib  544  baibd  548  bianabs  550  pm5.42  552  anclb  554  anabs5  675  annotanannot  847  pm5.33  848  pclem6  1043  moanimv  2647  moanim  2648  euan  2649  euanv  2652  ralanid  3113  rexanid  3114  r19.29  3128  rmoanid  3379  reuanid  3380  eueq3  3675  reu6  3690  reuan  3851  ifan  4542  dfopif  4836  notsep  5336  reusv2lem5  5375  dmopab2rex  5909  elpredg  6318  fvopab3g  6986  riota1a  7391  dfom2  7865  suppssr  8192  mpocurryd  8266  boxcutc  8940  funisfsupp  9328  dfac3  10106  eluz2  12869  elixx3g  13386  elfz2  13543  zmodid2  13934  shftfib  15111  dvdsssfz1  16377  modremain  16467  sadadd2lem2  16509  smumullem  16551  tltnle  18477  issubg  19193  resgrpisgrp  19215  sscntz  19397  pgrpsubgsymgbi  19479  qusecsub  19906  isrnghm  20524  rnghmval2  20527  issubrng  20633  issubrg  20657  lindsmm  21959  mdetunilem8  22757  mdetunilem9  22758  cmpsub  23538  txcnmpt  23762  hausdiag  23783  fbfinnfr  23979  elfilss  24014  fixufil  24060  ibladdlem  25960  iblabslem  25968  lenlts  27897  cusgruvtxb  29753  usgr0edg0rusgr  29906  rgrusgrprc  29920  rusgrnumwwlkslem  30302  eclclwwlkn1  30407  eupth2lem1  30550  pjimai  32509  chrelati  32697  metidv  34263  satfv1lem  35835  dmopab3rexdif  35878  copsex2b  37765  curf  38230  unccur  38235  cnambfre  38300  itg2addnclem2  38304  ibladdnclem  38308  iblabsnclem  38315  prjsprellsp  43326  expdiophlem1  43731  rfovcnvf1od  44713  fsovrfovd  44718  ntrneiel2  44795  odd2np1ALTV  48422  clnbupgrel  48582  dfvopnbgr2  48601  vopnbgrelself  48603  uzlidlring  48983  crngprmringidom  49089  islindeps  49216  elbigo2  49315  ralrals  50569  ralals  50575