Theorem ibar 536

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  biantrurd  540  baib  543  baibd  547  bianabs  549  pm5.42  551  anclb  553  anabs5  673  annotanannot  845  pm5.33  846  pclem6  1038  moanimv  2645  moanim  2646  euan  2647  euanv  2650  ralanid  3109  rexanid  3110  r19.29  3124  rmoanid  3376  reuanid  3377  eueq3  3673  reu6  3688  reuan  3849  ifan  4533  dfopif  4827  notzfaus  5319  reusv2lem5  5358  dmopab2rex  5891  elpredg  6298  fvopab3g  6966  riota1a  7371  dfom2  7844  suppssr  8170  mpocurryd  8244  boxcutc  8919  funisfsupp  9310  dfac3  10074  eluz2  12842  elixx3g  13359  elfz2  13516  zmodid2  13906  shftfib  15082  dvdsssfz1  16335  modremain  16425  sadadd2lem2  16467  smumullem  16509  tltnle  18435  issubg  19151  resgrpisgrp  19172  sscntz  19349  pgrpsubgsymgbi  19431  qusecsub  19858  isrnghm  20469  rnghmval2  20472  issubrng  20576  issubrg  20600  lindsmm  21860  mdetunilem8  22659  mdetunilem9  22660  cmpsub  23440  txcnmpt  23664  hausdiag  23685  fbfinnfr  23881  elfilss  23916  fixufil  23962  ibladdlem  25862  iblabslem  25870  lenlts  27793  cusgruvtxb  29569  usgr0edg0rusgr  29722  rgrusgrprc  29736  rusgrnumwwlkslem  30118  eclclwwlkn1  30223  eupth2lem1  30366  pjimai  32325  chrelati  32513  metidv  34150  satfv1lem  35676  dmopab3rexdif  35719  copsex2b  37596  curf  38061  unccur  38066  cnambfre  38131  itg2addnclem2  38135  ibladdnclem  38139  iblabsnclem  38146  prjsprellsp  43157  expdiophlem1  43562  rfovcnvf1od  44544  fsovrfovd  44549  ntrneiel2  44626  odd2np1ALTV  48260  clnbupgrel  48420  dfvopnbgr2  48439  vopnbgrelself  48441  uzlidlring  48821  islindeps  49039  elbigo2  49138