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  2647  moanim  2648  euan  2649  euanv  2652  ralanid  3114  rexanid  3115  r19.29  3129  rmoanid  3379  reuanid  3380  eueq3  3672  reu6  3687  reuan  3848  ifan  4539  dfopif  4840  notsep  5330  reusv2lem5  5369  dmopab2rex  5907  elpredg  6339  fvopab3g  7014  riota1a  7425  dfom2  7906  suppssr  8243  mpocurryd  8317  curf  8921  boxcutc  9000  funisfsupp  9390  dfac3  10230  eluz2  13001  elixx3g  13519  elfz2  13676  zmodid2  14069  shftfib  15257  dvdsssfz1  16520  modremain  16610  sadadd2lem2  16652  smumullem  16694  tltnle  18626  issubg  19368  resgrpisgrp  19390  sscntz  19573  pgrpsubgsymgbi  19655  qusecsub  20082  isrnghm  20704  rnghmval2  20707  issubrng  20832  issubrg  20856  lindsmm  22167  mdetunilem8  22967  mdetunilem9  22968  cmpsub  23751  txcnmpt  23976  hausdiag  23997  fbfinnfr  24193  elfilss  24228  fixufil  24274  ibladdlem  26173  iblabslem  26181  lenlts  28142  cusgruvtxb  30036  usgr0edg0rusgr  30189  rgrusgrprc  30203  rusgrnumwwlkslem  30594  eclclwwlkn1  30699  eupth2lem1  30852  pjimai  32811  chrelati  32999  metidv  34607  reu6f  35792  srepdflem1  36098  satfv1lem  36307  dmopab3rexdif  36350  copsex2b  38266  unccur  38731  cnambfre  38791  itg2addnclem2  38795  ibladdnclem  38799  iblabsnclem  38806  prjsprellsp  43843  expdiophlem1  44232  rfovcnvf1od  45207  fsovrfovd  45212  ntrneiel2  45289  odd2np1ALTV  48987  clnbupgrel  49147  dfvopnbgr2  49166  vopnbgrelself  49168  uzlidlring  49547  crngprmringidom  49653  islindeps  49780  elbigo2  49879  ralrals  51216  ralals  51222