Theorem ibar 524

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		pm3.2 462	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2		simpr 476	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	impbid1 215	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  biantrur  526  biantrurd  528  anclb  569  pm5.42  570  anabs5  868  pm5.33  940  bianabs  942  annotanannot  959  baib  964  baibd  968  pclem6  991  moanim  2558  euan  2559  eueq3  3414  reu6  3428  ifan  4167  dfopif  4430  reusv2lem5  4903  fvopab3g  6316  riota1a  6670  dfom2  7109  suppssr  7371  mpt2curryd  7440  boxcutc  7993  funisfsupp  8321  dfac3  8982  eluz2  11731  elixx3g  12226  elfz2  12371  zmodid2  12738  shftfib  13856  dvdsssfz1  15087  modremain  15179  sadadd2lem2  15219  smumullem  15261  issubg  17641  resgrpisgrp  17662  sscntz  17805  pgrpsubgsymgbi  17873  issubrg  18828  lindsmm  20215  mdetunilem8  20473  mdetunilem9  20474  cmpsub  21251  txcnmpt  21475  fbfinnfr  21692  elfilss  21727  fixufil  21773  ibladdlem  23631  iblabslem  23639  cusgruvtxb  26374  usgr0edg0rusgr  26527  rgrusgrprc  26541  rusgrnumwwlkslem  26936  eclclwwlkn1  27039  eupth2lem1  27196  pjimai  29163  chrelati  29351  tltnle  29790  metidv  30063  slenlt  32002  curf  33517  unccur  33522  cnambfre  33588  itg2addnclem2  33592  ibladdnclem  33596  iblabsnclem  33603  expdiophlem1  37905  rfovcnvf1od  38615  fsovrfovd  38620  ntrneiel2  38701  reuan  41501  odd2np1ALTV  41910  isrnghm  42217  rnghmval2  42220  uzlidlring  42254  islindeps  42567  elbigo2  42671