Theorem ibar 538

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biantrurd  542  baib  545  baibd  549  bianabs  551  pm5.42  553  anclb  555  anabs5  676  annotanannot  848  pm5.33  849  pclem6  1043  moanimv  2645  moanim  2646  euan  2647  euanv  2650  ralanid  3111  rexanid  3112  r19.29  3126  rmoanid  3376  reuanid  3377  eueq3  3669  reu6  3684  reuan  3844  ifan  4536  dfopif  4830  notsep  5325  reusv2lem5  5364  dmopab2rex  5899  elpredg  6311  fvopab3g  6980  riota1a  7391  dfom2  7868  suppssr  8196  mpocurryd  8270  curf  8874  boxcutc  8953  funisfsupp  9343  dfac3  10181  eluz2  12952  elixx3g  13470  elfz2  13627  zmodid2  14019  shftfib  15205  dvdsssfz1  16468  modremain  16558  sadadd2lem2  16600  smumullem  16642  tltnle  18574  issubg  19316  resgrpisgrp  19338  sscntz  19520  pgrpsubgsymgbi  19602  qusecsub  20029  isrnghm  20651  rnghmval2  20654  issubrng  20779  issubrg  20803  lindsmm  22114  mdetunilem8  22914  mdetunilem9  22915  cmpsub  23698  txcnmpt  23923  hausdiag  23944  fbfinnfr  24140  elfilss  24175  fixufil  24221  ibladdlem  26120  iblabslem  26128  lenlts  28091  cusgruvtxb  29985  usgr0edg0rusgr  30138  rgrusgrprc  30152  rusgrnumwwlkslem  30543  eclclwwlkn1  30648  eupth2lem1  30801  pjimai  32760  chrelati  32948  metidv  34506  satfv1lem  36096  dmopab3rexdif  36139  copsex2b  38029  unccur  38494  cnambfre  38554  itg2addnclem2  38558  ibladdnclem  38562  iblabsnclem  38569  prjsprellsp  43601  expdiophlem1  43981  rfovcnvf1od  44963  fsovrfovd  44968  ntrneiel2  45045  odd2np1ALTV  48716  clnbupgrel  48876  dfvopnbgr2  48895  vopnbgrelself  48897  uzlidlring  49276  crngprmringidom  49382  islindeps  49509  elbigo2  49608  ralrals  50848  ralals  50854