Theorem ibar 529

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 528	. 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  533  baib  536  baibd  540  bianabs  542  pm5.42  544  anclb  546  anabs5  659  annotanannot  831  pm5.33  832  pclem6  1020  moanimv  2672  moanim  2673  euan  2674  euanv  2678  ralanid  3135  rexanid  3216  eueq3  3638  reu6  3651  reuan  3808  ifan  4432  dfopif  4707  notzfaus  5153  reusv2lem5  5194  dmopab2rex  5672  fvopab3g  6630  riota1a  6996  dfom2  7438  suppssr  7712  mpocurryd  7786  boxcutc  8353  funisfsupp  8684  dfac3  9393  eluz2  12099  elixx3g  12601  elfz2  12749  zmodid2  13117  shftfib  14265  dvdsssfz1  15501  modremain  15592  sadadd2lem2  15632  smumullem  15674  issubg  18033  resgrpisgrp  18054  sscntz  18197  pgrpsubgsymgbi  18266  issubrg  19225  lindsmm  20654  mdetunilem8  20912  mdetunilem9  20913  cmpsub  21692  txcnmpt  21916  hausdiag  21937  fbfinnfr  22133  elfilss  22168  fixufil  22214  ibladdlem  24103  iblabslem  24111  cusgruvtxb  26887  usgr0edg0rusgr  27040  rgrusgrprc  27054  rusgrnumwwlkslem  27435  eclclwwlkn1  27541  eupth2lem1  27685  pjimai  29644  chrelati  29832  tltnle  30323  metidv  30749  satfv1lem  32217  dmopab3rexdif  32260  slenlt  32840  curf  34401  unccur  34406  cnambfre  34471  itg2addnclem2  34475  ibladdnclem  34479  iblabsnclem  34486  prjsprellsp  38758  expdiophlem1  39103  rfovcnvf1od  39835  fsovrfovd  39840  ntrneiel2  39921  odd2np1ALTV  43321  isrnghm  43641  rnghmval2  43644  uzlidlring  43678  islindeps  43988  elbigo2  44093