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  2612  moanim  2613  euan  2614  euanv  2617  ralanid  3077  rexanid  3078  r19.29  3092  rmoanid  3355  reuanid  3356  eueq3  3673  reu6  3688  reuan  3850  ifan  4532  dfopif  4824  notzfaus  5305  reusv2lem5  5344  dmopab2rex  5864  elpredg  6267  fvopab3g  6929  riota1a  7332  dfom2  7808  suppssr  8135  mpocurryd  8209  boxcutc  8875  funisfsupp  9276  dfac3  10034  eluz2  12759  elixx3g  13279  elfz2  13435  zmodid2  13821  shftfib  14997  dvdsssfz1  16247  modremain  16337  sadadd2lem2  16379  smumullem  16421  tltnle  18344  issubg  19023  resgrpisgrp  19044  sscntz  19223  pgrpsubgsymgbi  19305  qusecsub  19732  isrnghm  20344  rnghmval2  20347  issubrng  20450  issubrg  20474  lindsmm  21753  mdetunilem8  22522  mdetunilem9  22523  cmpsub  23303  txcnmpt  23527  hausdiag  23548  fbfinnfr  23744  elfilss  23779  fixufil  23825  ibladdlem  25737  iblabslem  25745  slenlt  27680  cusgruvtxb  29385  usgr0edg0rusgr  29539  rgrusgrprc  29553  rusgrnumwwlkslem  29932  eclclwwlkn1  30037  eupth2lem1  30180  pjimai  32138  chrelati  32326  bian1d  32418  metidv  33861  satfv1lem  35337  dmopab3rexdif  35380  copsex2b  37116  curf  37580  unccur  37585  cnambfre  37650  itg2addnclem2  37654  ibladdnclem  37658  iblabsnclem  37665  prjsprellsp  42587  expdiophlem1  42997  rfovcnvf1od  43980  fsovrfovd  43985  ntrneiel2  44062  odd2np1ALTV  47662  clnbupgrel  47822  dfvopnbgr2  47841  vopnbgrelself  47843  uzlidlring  48223  islindeps  48442  elbigo2  48541