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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  biantrurd  532  baib  535  baibd  539  bianabs  541  pm5.42  543  anclb  545  anabs5  659  annotanannot  831  pm5.33  832  pclem6  1022  moanimv  2621  moanim  2622  euan  2623  euanv  2626  ralanid  3093  rexanid  3182  eueq3  3641  reu6  3656  reuan  3825  ifan  4509  dfopifOLD  4798  notzfaus  5280  reusv2lem5  5320  dmopab2rex  5815  elpredg  6205  fvopab3g  6852  riota1a  7235  dfom2  7689  suppssr  7983  mpocurryd  8056  boxcutc  8687  funisfsupp  9063  dfac3  9808  eluz2  12517  elixx3g  13021  elfz2  13175  zmodid2  13547  shftfib  14711  dvdsssfz1  15955  modremain  16045  sadadd2lem2  16085  smumullem  16127  tltnle  18055  issubg  18670  resgrpisgrp  18691  sscntz  18847  pgrpsubgsymgbi  18931  issubrg  19939  lindsmm  20945  mdetunilem8  21676  mdetunilem9  21677  cmpsub  22459  txcnmpt  22683  hausdiag  22704  fbfinnfr  22900  elfilss  22935  fixufil  22981  ibladdlem  24889  iblabslem  24897  cusgruvtxb  27692  usgr0edg0rusgr  27845  rgrusgrprc  27859  rusgrnumwwlkslem  28235  eclclwwlkn1  28340  eupth2lem1  28483  pjimai  30439  chrelati  30627  metidv  31744  satfv1lem  33224  dmopab3rexdif  33267  slenlt  33882  copsex2b  35238  curf  35682  unccur  35687  cnambfre  35752  itg2addnclem2  35756  ibladdnclem  35760  iblabsnclem  35767  prjsprellsp  40371  expdiophlem1  40759  rfovcnvf1od  41501  fsovrfovd  41506  ntrneiel2  41585  odd2np1ALTV  45014  isrnghm  45338  rnghmval2  45341  uzlidlring  45375  islindeps  45682  elbigo2  45786