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  708  cases  1043  truan  1548  2sb5rf  2480  euae  2663  rexv  3517  reuv  3518  rmov  3519  rabab  3520  euxfrw  3743  euxfr  3745  euind  3746  dfdif3OLD  4141  ddif  4164  nssinpss  4286  nsspssun  4287  notabw  4332  vss  4469  reuprg0  4727  reuprg  4728  difsnpss  4832  sspr  4860  sstp  4861  disjprg  5162  mptv  5282  reusv2lem5  5420  oteqex2  5518  dfid4  5594  intirr  6150  xpcan  6207  resssxp  6301  fvopab6  7063  fnressn  7192  riotav  7409  mpov  7562  sorpss  7763  opabn1stprc  8099  fparlem2  8154  fnsuppres  8232  brtpos0  8274  naddrid  8739  sup0riota  9534  genpass  11078  nnwos  12980  hashbclem  14501  ccatlcan  14766  clim0  15552  gcd0id  16565  isdomn3  20737  pjfval2  21752  mat1dimbas  22499  pmatcollpw2lem  22804  isbasis3g  22977  opnssneib  23144  ssidcn  23284  qtopcld  23742  mdegleb  26123  vieta1  26372  lgsne0  27397  axpasch  28974  0wlk  30148  0clwlk  30162  shlesb1i  31418  chnlei  31517  pjneli  31755  cvexchlem  32400  dmdbr5ati  32454  elimifd  32566  fzo0opth  32810  1arithidom  33530  lmxrge0  33898  cntnevol  34192  bnj110  34834  goeleq12bg  35317  fmlafvel  35353  elpotr  35745  dfbigcup2  35863  bj-rexvw  36846  bj-rababw  36847  bj-brab2a1  37115  finxpreclem4  37360  wl-cases2-dnf  37466  wl-euae  37471  wl-dfclab  37550  cnambfre  37628  triantru3  38184  lub0N  39145  glb0N  39149  cvlsupr3  39300  ifpdfor2  43423  ifpdfor  43427  ifpim1  43431  ifpid2  43433  ifpim2  43434  ifpid2g  43455  ifpid1g  43456  ifpim23g  43457  ifpim1g  43463  ifpimimb  43466  rp-isfinite6  43480  rababg  43536  relnonrel  43549  dffrege115  43940  funressnfv  46958  dfnelbr2  47188  edgusgrclnbfin  47714