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  2650  moanim  2651  euan  2652  euanv  2655  ralanid  3116  rexanid  3117  r19.29  3131  rmoanid  3382  reuanid  3383  eueq3  3677  reu6  3692  reuan  3853  ifan  4546  dfopif  4840  notsep  5339  reusv2lem5  5378  dmopab2rex  5912  elpredg  6323  fvopab3g  6991  riota1a  7402  dfom2  7873  suppssr  8200  mpocurryd  8274  boxcutc  8948  funisfsupp  9337  dfac3  10124  eluz2  12886  elixx3g  13403  elfz2  13560  zmodid2  13952  shftfib  15135  dvdsssfz1  16401  modremain  16491  sadadd2lem2  16533  smumullem  16575  tltnle  18501  issubg  19223  resgrpisgrp  19245  sscntz  19427  pgrpsubgsymgbi  19509  qusecsub  19936  isrnghm  20556  rnghmval2  20559  issubrng  20683  issubrg  20707  lindsmm  22015  mdetunilem8  22813  mdetunilem9  22814  cmpsub  23594  txcnmpt  23818  hausdiag  23839  fbfinnfr  24035  elfilss  24070  fixufil  24116  ibladdlem  26016  iblabslem  26024  lenlts  27953  cusgruvtxb  29809  usgr0edg0rusgr  29962  rgrusgrprc  29976  rusgrnumwwlkslem  30358  eclclwwlkn1  30463  eupth2lem1  30606  pjimai  32565  chrelati  32753  metidv  34313  satfv1lem  35875  dmopab3rexdif  35918  copsex2b  37825  curf  38290  unccur  38295  cnambfre  38360  itg2addnclem2  38364  ibladdnclem  38368  iblabsnclem  38375  prjsprellsp  43384  expdiophlem1  43789  rfovcnvf1od  44771  fsovrfovd  44776  ntrneiel2  44853  odd2np1ALTV  48480  clnbupgrel  48640  dfvopnbgr2  48659  vopnbgrelself  48661  uzlidlring  49041  crngprmringidom  49147  islindeps  49274  elbigo2  49373  ralrals  50627  ralals  50633