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

This theorem is referenced by:  mpbiran  710  cases  1043  truan  1553  2sb5rf  2477  euae  2661  rexv  3470  reuv  3471  rmov  3472  rabab  3473  euxfrw  3681  euxfr  3683  euind  3684  dfdif3OLD  4072  ddif  4095  nssinpss  4221  nsspssun  4222  notabw  4267  vss  4400  reuprg0  4661  reuprg  4662  difsnpss  4765  sspr  4793  sstp  4794  disjprg  5096  mptv  5206  reusv2lem5  5349  oteqex2  5455  dfid4  5528  intirr  6083  xpcan  6142  resssxp  6236  fvopab6  6984  fnressn  7113  riotav  7330  mpov  7480  sorpss  7683  opabn1stprc  8012  fparlem2  8065  fnsuppres  8143  brtpos0  8185  naddrid  8621  sup0riota  9381  genpass  10932  nnwos  12840  hashbclem  14387  ccatlcan  14653  clim0  15441  gcd0id  16458  isdomn3  20660  pjfval2  21676  mat1dimbas  22428  pmatcollpw2lem  22733  isbasis3g  22905  opnssneib  23071  ssidcn  23211  qtopcld  23669  mdegleb  26037  vieta1  26288  lgsne0  27314  axpasch  29026  0wlk  30203  0clwlk  30217  shlesb1i  31474  chnlei  31573  pjneli  31811  cvexchlem  32456  dmdbr5ati  32510  elimifd  32630  fzo0opth  32894  1arithidom  33630  lmxrge0  34130  cntnevol  34406  bnj110  35034  vonf1owev  35324  goeleq12bg  35565  fmlafvel  35601  elpotr  35995  dfbigcup2  36113  bj-alnnf  36980  bj-rexvw  37128  bj-rababw  37129  bj-brab2a1  37404  finxpreclem4  37649  wl-cases2-dnf  37767  wl-euae  37772  wl-dfclab  37840  cnambfre  37919  triantru3  38487  lub0N  39565  glb0N  39569  cvlsupr3  39720  ifpdfor2  43817  ifpdfor  43821  ifpim1  43825  ifpid2  43827  ifpim2  43828  ifpid2g  43849  ifpid1g  43850  ifpim23g  43851  ifpim1g  43857  ifpimimb  43860  rp-isfinite6  43874  rababg  43930  relnonrel  43943  dffrege115  44334  chnsubseqwl  47237  funressnfv  47403  dfnelbr2  47633  edgusgrclnbfin  48202