Theorem biantrur 530

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)

Hypothesis

Ref	Expression
biantrur.1	⊢ 𝜑

Assertion

Ref	Expression
biantrur	⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

Proof of Theorem biantrur

Step	Hyp	Ref	Expression
1		biantrur.1	. . 3 ⊢ 𝜑
2	1	biantru 529	. 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))
3	2	biancomi 462	1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  mpbiran  708  cases  1041  truan  1545  2sb5rf  2466  euae  2650  rexv  3495  reuv  3496  rmov  3497  rabab  3498  euxfrw  3714  euxfr  3716  euind  3717  dfdif3  4110  ddif  4132  nssinpss  4252  nsspssun  4253  notabw  4299  vss  4439  reuprg0  4702  reuprg  4703  difsnpss  4806  sspr  4832  sstp  4833  disjprgw  5137  disjprg  5138  mptv  5258  reusv2lem5  5396  oteqex2  5495  dfid4  5571  intirr  6118  xpcan  6174  resssxp  6268  fvopab6  7033  fnressn  7161  riotav  7375  mpov  7526  sorpss  7727  opabn1stprc  8056  fparlem2  8112  fnsuppres  8189  brtpos0  8232  naddrid  8697  sup0riota  9482  genpass  11026  nnwos  12923  hashbclem  14437  ccatlcan  14694  clim0  15476  gcd0id  16487  isdomn3  21241  pjfval2  21636  mat1dimbas  22367  pmatcollpw2lem  22672  isbasis3g  22845  opnssneib  23012  ssidcn  23152  qtopcld  23610  mdegleb  25993  vieta1  26240  lgsne0  27261  axpasch  28745  0wlk  29919  0clwlk  29933  shlesb1i  31189  chnlei  31288  pjneli  31526  cvexchlem  32171  dmdbr5ati  32225  elimifd  32327  lmxrge0  33543  cntnevol  33837  bnj110  34479  goeleq12bg  34949  fmlafvel  34985  elpotr  35367  dfbigcup2  35485  bj-rexvw  36348  bj-rababw  36349  bj-brab2a1  36618  finxpreclem4  36863  wl-cases2-dnf  36969  wl-euae  36974  wl-dfclab  37052  cnambfre  37130  triantru3  37688  lub0N  38650  glb0N  38654  cvlsupr3  38805  ifpdfor2  42863  ifpdfor  42867  ifpim1  42871  ifpid2  42873  ifpim2  42874  ifpid2g  42895  ifpid1g  42896  ifpim23g  42897  ifpim1g  42903  ifpimimb  42906  rp-isfinite6  42920  rababg  42976  relnonrel  42989  dffrege115  43380  funressnfv  46397  dfnelbr2  46625