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  1552  2sb5rf  2476  euae  2660  rexv  3468  reuv  3469  rmov  3470  rabab  3471  euxfrw  3679  euxfr  3681  euind  3682  dfdif3OLD  4070  ddif  4093  nssinpss  4219  nsspssun  4220  notabw  4265  vss  4398  reuprg0  4659  reuprg  4660  difsnpss  4763  sspr  4791  sstp  4792  disjprg  5094  mptv  5204  reusv2lem5  5347  oteqex2  5447  dfid4  5520  intirr  6075  xpcan  6134  resssxp  6228  fvopab6  6975  fnressn  7103  riotav  7320  mpov  7470  sorpss  7673  opabn1stprc  8002  fparlem2  8055  fnsuppres  8133  brtpos0  8175  naddrid  8611  sup0riota  9369  genpass  10920  nnwos  12828  hashbclem  14375  ccatlcan  14641  clim0  15429  gcd0id  16446  isdomn3  20648  pjfval2  21664  mat1dimbas  22416  pmatcollpw2lem  22721  isbasis3g  22893  opnssneib  23059  ssidcn  23199  qtopcld  23657  mdegleb  26025  vieta1  26276  lgsne0  27302  axpasch  29014  0wlk  30191  0clwlk  30205  shlesb1i  31461  chnlei  31560  pjneli  31798  cvexchlem  32443  dmdbr5ati  32497  elimifd  32618  fzo0opth  32883  1arithidom  33618  lmxrge0  34109  cntnevol  34385  bnj110  35014  vonf1owev  35302  goeleq12bg  35543  fmlafvel  35579  elpotr  35973  dfbigcup2  36091  bj-rexvw  37081  bj-rababw  37082  bj-brab2a1  37354  finxpreclem4  37599  wl-cases2-dnf  37717  wl-euae  37722  wl-dfclab  37790  cnambfre  37869  triantru3  38432  lub0N  39449  glb0N  39453  cvlsupr3  39604  ifpdfor2  43702  ifpdfor  43706  ifpim1  43710  ifpid2  43712  ifpim2  43713  ifpid2g  43734  ifpid1g  43735  ifpim23g  43736  ifpim1g  43742  ifpimimb  43745  rp-isfinite6  43759  rababg  43815  relnonrel  43828  dffrege115  44219  chnsubseqwl  47123  funressnfv  47289  dfnelbr2  47519  edgusgrclnbfin  48088