Theorem ibar 518

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

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

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 383

This theorem is referenced by:  biantrur  520  biantrurd  522  baib  525  baibd  529  bianabs  531  pm5.42  533  anclb  535  anabs5  642  annotanannot  830  pm5.33  831  pclem6  1011  moanim  2678  euan  2679  eueq3  3533  reu6  3547  ifan  4274  dfopif  4537  reusv2lem5  5003  fvopab3g  6421  riota1a  6775  dfom2  7217  suppssr  7481  mpt2curryd  7550  boxcutc  8108  funisfsupp  8439  dfac3  9147  eluz2  11898  elixx3g  12392  elfz2  12539  zmodid2  12905  shftfib  14019  dvdsssfz1  15248  modremain  15339  sadadd2lem2  15379  smumullem  15421  issubg  17801  resgrpisgrp  17822  sscntz  17965  pgrpsubgsymgbi  18033  issubrg  18989  lindsmm  20383  mdetunilem8  20642  mdetunilem9  20643  cmpsub  21423  txcnmpt  21647  fbfinnfr  21864  elfilss  21899  fixufil  21945  ibladdlem  23805  iblabslem  23813  cusgruvtxb  26552  usgr0edg0rusgr  26705  rgrusgrprc  26719  rusgrnumwwlkslem  27117  eclclwwlkn1  27232  eupth2lem1  27397  pjimai  29374  chrelati  29562  tltnle  30001  metidv  30274  slenlt  32213  curf  33719  unccur  33724  cnambfre  33789  itg2addnclem2  33793  ibladdnclem  33797  iblabsnclem  33804  expdiophlem1  38114  rfovcnvf1od  38824  fsovrfovd  38829  ntrneiel2  38910  reuan  41697  odd2np1ALTV  42110  isrnghm  42417  rnghmval2  42420  uzlidlring  42454  islindeps  42767  elbigo2  42871