Theorem ibar 532

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 531	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
2	1	biancomd 467	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  biantrurd  536  baib  539  baibd  543  bianabs  545  pm5.42  547  anclb  549  anabs5  663  annotanannot  835  pm5.33  836  pclem6  1026  moanimv  2620  moanim  2621  euan  2622  euanv  2625  ralanid  3091  rexanid  3175  eueq3  3624  reu6  3639  reuan  3808  ifan  4492  dfopifOLD  4781  notzfaus  5254  reusv2lem5  5295  dmopab2rex  5786  elpredg  6173  fvopab3g  6813  riota1a  7193  dfom2  7646  suppssr  7938  mpocurryd  8011  boxcutc  8622  funisfsupp  8990  dfac3  9735  eluz2  12444  elixx3g  12948  elfz2  13102  zmodid2  13472  shftfib  14635  dvdsssfz1  15879  modremain  15969  sadadd2lem2  16009  smumullem  16051  tltnle  17928  issubg  18543  resgrpisgrp  18564  sscntz  18720  pgrpsubgsymgbi  18800  issubrg  19800  lindsmm  20790  mdetunilem8  21516  mdetunilem9  21517  cmpsub  22297  txcnmpt  22521  hausdiag  22542  fbfinnfr  22738  elfilss  22773  fixufil  22819  ibladdlem  24717  iblabslem  24725  cusgruvtxb  27510  usgr0edg0rusgr  27663  rgrusgrprc  27677  rusgrnumwwlkslem  28053  eclclwwlkn1  28158  eupth2lem1  28301  pjimai  30257  chrelati  30445  metidv  31556  satfv1lem  33037  dmopab3rexdif  33080  slenlt  33692  copsex2b  35046  curf  35492  unccur  35497  cnambfre  35562  itg2addnclem2  35566  ibladdnclem  35570  iblabsnclem  35577  prjsprellsp  40158  expdiophlem1  40546  rfovcnvf1od  41289  fsovrfovd  41294  ntrneiel2  41373  odd2np1ALTV  44799  isrnghm  45123  rnghmval2  45126  uzlidlring  45160  islindeps  45467  elbigo2  45571