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  2467  euae  2651  rexv  3496  reuv  3497  rmov  3498  rabab  3499  euxfrw  3715  euxfr  3717  euind  3718  dfdif3  4111  ddif  4133  nssinpss  4253  nsspssun  4254  notabw  4300  vss  4440  reuprg0  4703  reuprg  4704  difsnpss  4807  sspr  4833  sstp  4834  disjprgw  5138  disjprg  5139  mptv  5259  reusv2lem5  5397  oteqex2  5496  dfid4  5572  intirr  6119  xpcan  6175  resssxp  6269  fvopab6  7034  fnressn  7162  riotav  7376  mpov  7527  sorpss  7728  opabn1stprc  8057  fparlem2  8113  fnsuppres  8190  brtpos0  8233  naddrid  8698  sup0riota  9483  genpass  11027  nnwos  12924  hashbclem  14438  ccatlcan  14695  clim0  15477  gcd0id  16488  isdomn3  21242  pjfval2  21637  mat1dimbas  22368  pmatcollpw2lem  22673  isbasis3g  22846  opnssneib  23013  ssidcn  23153  qtopcld  23611  mdegleb  25994  vieta1  26241  lgsne0  27262  axpasch  28746  0wlk  29920  0clwlk  29934  shlesb1i  31190  chnlei  31289  pjneli  31527  cvexchlem  32172  dmdbr5ati  32226  elimifd  32328  lmxrge0  33548  cntnevol  33842  bnj110  34484  goeleq12bg  34954  fmlafvel  34990  elpotr  35372  dfbigcup2  35490  bj-rexvw  36353  bj-rababw  36354  bj-brab2a1  36623  finxpreclem4  36868  wl-cases2-dnf  36974  wl-euae  36979  wl-dfclab  37058  cnambfre  37136  triantru3  37694  lub0N  38656  glb0N  38660  cvlsupr3  38811  ifpdfor2  42882  ifpdfor  42886  ifpim1  42890  ifpid2  42892  ifpim2  42893  ifpid2g  42914  ifpid1g  42915  ifpim23g  42916  ifpim1g  42922  ifpimimb  42925  rp-isfinite6  42939  rababg  42995  relnonrel  43008  dffrege115  43399  funressnfv  46416  dfnelbr2  46644