Theorem ibar 520

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 457	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2		simpr 473	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3	1, 2	impbid1 216	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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

This theorem is referenced by:  biantrur  522  biantrurd  524  baib  527  baibd  531  bianabs  533  pm5.42  535  anclb  537  anabs5  645  annotanannot  854  pm5.33  855  pclem6  1040  moanim  2693  euan  2694  eueq3  3579  reu6  3593  ifan  4330  dfopif  4592  reusv2lem5  5071  fvopab3g  6494  riota1a  6850  dfom2  7293  suppssr  7557  mpt2curryd  7626  boxcutc  8184  funisfsupp  8515  dfac3  9223  eluz2  11906  elixx3g  12402  elfz2  12552  zmodid2  12918  shftfib  14031  dvdsssfz1  15259  modremain  15347  sadadd2lem2  15387  smumullem  15429  issubg  17792  resgrpisgrp  17813  sscntz  17956  pgrpsubgsymgbi  18024  issubrg  18980  lindsmm  20373  mdetunilem8  20632  mdetunilem9  20633  cmpsub  21413  txcnmpt  21637  fbfinnfr  21854  elfilss  21889  fixufil  21935  ibladdlem  23796  iblabslem  23804  cusgruvtxb  26542  usgr0edg0rusgr  26695  rgrusgrprc  26709  rusgrnumwwlkslem  27107  eclclwwlkn1  27222  eupth2lem1  27387  pjimai  29359  chrelati  29547  tltnle  29983  metidv  30256  slenlt  32193  curf  33695  unccur  33700  cnambfre  33765  itg2addnclem2  33769  ibladdnclem  33773  iblabsnclem  33780  expdiophlem1  38083  rfovcnvf1od  38792  fsovrfovd  38797  ntrneiel2  38878  reuan  41686  odd2np1ALTV  42154  isrnghm  42454  rnghmval2  42457  uzlidlring  42491  islindeps  42804  elbigo2  42908