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  2644  moanim  2645  euan  2646  euanv  2649  ralanid  3110  rexanid  3111  r19.29  3125  rmoanid  3375  reuanid  3376  eueq3  3668  reu6  3683  reuan  3843  ifan  4535  dfopif  4836  notsep  5324  reusv2lem5  5363  dmopab2rex  5898  elpredg  6318  fvopab3g  6989  riota1a  7400  dfom2  7880  suppssr  8216  mpocurryd  8290  curf  8894  boxcutc  8973  funisfsupp  9363  dfac3  10204  eluz2  12975  elixx3g  13493  elfz2  13650  zmodid2  14043  shftfib  15231  dvdsssfz1  16494  modremain  16584  sadadd2lem2  16626  smumullem  16668  tltnle  18600  issubg  19342  resgrpisgrp  19364  sscntz  19546  pgrpsubgsymgbi  19628  qusecsub  20055  isrnghm  20677  rnghmval2  20680  issubrng  20805  issubrg  20829  lindsmm  22140  mdetunilem8  22940  mdetunilem9  22941  cmpsub  23724  txcnmpt  23949  hausdiag  23970  fbfinnfr  24166  elfilss  24201  fixufil  24247  ibladdlem  26146  iblabslem  26154  lenlts  28115  cusgruvtxb  30009  usgr0edg0rusgr  30162  rgrusgrprc  30176  rusgrnumwwlkslem  30567  eclclwwlkn1  30672  eupth2lem1  30825  pjimai  32784  chrelati  32972  metidv  34571  reu6f  35756  srepdflem1  36005  satfv1lem  36214  dmopab3rexdif  36257  copsex2b  38155  unccur  38620  cnambfre  38680  itg2addnclem2  38684  ibladdnclem  38688  iblabsnclem  38695  prjsprellsp  43733  expdiophlem1  44122  rfovcnvf1od  45098  fsovrfovd  45103  ntrneiel2  45180  odd2np1ALTV  48866  clnbupgrel  49026  dfvopnbgr2  49045  vopnbgrelself  49047  uzlidlring  49426  crngprmringidom  49532  islindeps  49659  elbigo2  49758  ralrals  51073  ralals  51079