Theorem ibar 537

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

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

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 401

This theorem is referenced by:  biantrurd  541  baib  544  baibd  548  bianabs  550  pm5.42  552  anclb  554  anabs5  675  annotanannot  847  pm5.33  848  pclem6  1041  moanimv  2649  moanim  2650  euan  2651  euanv  2654  ralanid  3113  rexanid  3114  r19.29  3128  rmoanid  3380  reuanid  3381  eueq3  3677  reu6  3692  reuan  3852  ifan  4537  dfopif  4831  notzfaus  5325  reusv2lem5  5364  dmopab2rex  5898  elpredg  6306  fvopab3g  6974  riota1a  7379  dfom2  7852  suppssr  8179  mpocurryd  8253  boxcutc  8927  funisfsupp  9315  dfac3  10093  eluz2  12859  elixx3g  13376  elfz2  13533  zmodid2  13923  shftfib  15099  dvdsssfz1  16366  modremain  16456  sadadd2lem2  16498  smumullem  16540  tltnle  18466  issubg  19183  resgrpisgrp  19205  sscntz  19387  pgrpsubgsymgbi  19469  qusecsub  19896  isrnghm  20514  rnghmval2  20517  issubrng  20623  issubrg  20647  lindsmm  21938  mdetunilem8  22737  mdetunilem9  22738  cmpsub  23518  txcnmpt  23742  hausdiag  23763  fbfinnfr  23959  elfilss  23994  fixufil  24040  ibladdlem  25940  iblabslem  25948  lenlts  27874  cusgruvtxb  29681  usgr0edg0rusgr  29834  rgrusgrprc  29848  rusgrnumwwlkslem  30230  eclclwwlkn1  30335  eupth2lem1  30478  pjimai  32437  chrelati  32625  metidv  34199  satfv1lem  35725  dmopab3rexdif  35768  copsex2b  37644  curf  38109  unccur  38114  cnambfre  38179  itg2addnclem2  38183  ibladdnclem  38187  iblabsnclem  38194  prjsprellsp  43205  expdiophlem1  43610  rfovcnvf1od  44592  fsovrfovd  44597  ntrneiel2  44674  odd2np1ALTV  48294  clnbupgrel  48454  dfvopnbgr2  48473  vopnbgrelself  48475  uzlidlring  48855  crngprmringidom  48961  islindeps  49084  elbigo2  49183