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  709  cases  1042  truan  1551  2sb5rf  2470  euae  2653  rexv  3472  reuv  3473  rmov  3474  rabab  3475  euxfrw  3689  euxfr  3691  euind  3692  dfdif3OLD  4077  ddif  4100  nssinpss  4226  nsspssun  4227  notabw  4272  vss  4405  reuprg0  4662  reuprg  4663  difsnpss  4767  sspr  4795  sstp  4796  disjprg  5098  mptv  5208  reusv2lem5  5352  oteqex2  5454  dfid4  5527  intirr  6079  xpcan  6137  resssxp  6231  fvopab6  6984  fnressn  7112  riotav  7331  mpov  7481  sorpss  7684  opabn1stprc  8016  fparlem2  8069  fnsuppres  8147  brtpos0  8189  naddrid  8624  sup0riota  9393  genpass  10938  nnwos  12850  hashbclem  14393  ccatlcan  14659  clim0  15448  gcd0id  16465  isdomn3  20635  pjfval2  21651  mat1dimbas  22392  pmatcollpw2lem  22697  isbasis3g  22869  opnssneib  23035  ssidcn  23175  qtopcld  23633  mdegleb  26002  vieta1  26253  lgsne0  27279  axpasch  28921  0wlk  30095  0clwlk  30109  shlesb1i  31365  chnlei  31464  pjneli  31702  cvexchlem  32347  dmdbr5ati  32401  elimifd  32522  fzo0opth  32778  1arithidom  33501  lmxrge0  33935  cntnevol  34211  bnj110  34841  vonf1owev  35088  goeleq12bg  35329  fmlafvel  35365  elpotr  35762  dfbigcup2  35880  bj-rexvw  36861  bj-rababw  36862  bj-brab2a1  37130  finxpreclem4  37375  wl-cases2-dnf  37493  wl-euae  37498  wl-dfclab  37577  cnambfre  37655  triantru3  38211  lub0N  39175  glb0N  39179  cvlsupr3  39330  ifpdfor2  43443  ifpdfor  43447  ifpim1  43451  ifpid2  43453  ifpim2  43454  ifpid2g  43475  ifpid1g  43476  ifpim23g  43477  ifpim1g  43483  ifpimimb  43486  rp-isfinite6  43500  rababg  43556  relnonrel  43569  dffrege115  43960  funressnfv  47037  dfnelbr2  47267  edgusgrclnbfin  47835