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  663  annotanannot  834  pm5.33  835  pclem6  1027  moanimv  2613  moanim  2614  euan  2615  euanv  2618  ralanid  3078  rexanid  3079  r19.29  3093  rmoanid  3354  reuanid  3355  eueq3  3668  reu6  3683  reuan  3845  ifan  4527  dfopif  4820  notzfaus  5299  reusv2lem5  5338  dmopab2rex  5855  elpredg  6258  fvopab3g  6919  riota1a  7320  dfom2  7793  suppssr  8120  mpocurryd  8194  boxcutc  8860  funisfsupp  9246  dfac3  10004  eluz2  12730  elixx3g  13250  elfz2  13406  zmodid2  13795  shftfib  14971  dvdsssfz1  16221  modremain  16311  sadadd2lem2  16353  smumullem  16395  tltnle  18318  issubg  19031  resgrpisgrp  19052  sscntz  19231  pgrpsubgsymgbi  19313  qusecsub  19740  isrnghm  20352  rnghmval2  20355  issubrng  20455  issubrg  20479  lindsmm  21758  mdetunilem8  22527  mdetunilem9  22528  cmpsub  23308  txcnmpt  23532  hausdiag  23553  fbfinnfr  23749  elfilss  23784  fixufil  23830  ibladdlem  25741  iblabslem  25749  slenlt  27684  cusgruvtxb  29393  usgr0edg0rusgr  29547  rgrusgrprc  29561  rusgrnumwwlkslem  29940  eclclwwlkn1  30045  eupth2lem1  30188  pjimai  32146  chrelati  32334  bian1d  32425  metidv  33895  satfv1lem  35374  dmopab3rexdif  35417  copsex2b  37153  curf  37617  unccur  37622  cnambfre  37687  itg2addnclem2  37691  ibladdnclem  37695  iblabsnclem  37702  prjsprellsp  42623  expdiophlem1  43033  rfovcnvf1od  44016  fsovrfovd  44021  ntrneiel2  44098  odd2np1ALTV  47684  clnbupgrel  47844  dfvopnbgr2  47863  vopnbgrelself  47865  uzlidlring  48245  islindeps  48464  elbigo2  48563