Theorem biantrur 539

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 538	. 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))
3	2	biancomi 467	1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpbiran  721  cases  1056  truan  1578  2sb5rf  2510  euae  2693  rexv  3490  reuv  3491  rmov  3492  rabab  3493  euxfrw  3693  euxfr  3695  euind  3696  dfdif3OLD  4081  ddif  4103  nssinpss  4228  nsspssun  4229  notabw  4274  vss  4371  reuprg0  4673  reuprg  4674  difsnpss  4779  sspr  4804  sstp  4805  disjprg  5109  mptv  5221  reusv2lem5  5374  oteqex2  5483  dfid4  5558  intirr  6119  xpcan  6175  resssxp  6272  fvopab6  7025  fnressn  7156  riotav  7373  mpov  7523  sorpss  7726  opabn1stprc  8054  fparlem2  8107  fnsuppres  8186  brtpos0  8228  naddrid  8669  sup0riota  9425  genpass  10993  nnwos  12938  hashbclem  14488  ccatlcan  14754  clim0  15556  gcd0id  16576  isdomn3  20798  pjfval2  21827  mat1dimbas  22597  pmatcollpw2lem  22902  isbasis3g  23074  opnssneib  23240  ssidcn  23380  qtopcld  23838  mdegleb  26189  vieta1  26441  lgsne0  27464  axpasch  29231  0wlk  30407  0clwlk  30421  shlesb1i  31678  chnlei  31777  pjneli  32015  cvexchlem  32660  dmdbr5ati  32714  elimifd  32829  fzo0opth  33088  1arithidom  33771  lmxrge0  34286  cntnevol  34562  bnj110  35190  vonf1wev  35490  vonf1owevOLD  35492  goeleq12bg  35739  fmlafvel  35775  elpotr  36169  dfbigcup2  36287  mh-regprimbi  36944  bj-alnnf  37250  bj-rexvw  37403  bj-rababw  37404  bj-brab2a1  37680  finxpreclem4  37927  wl-cases2-dnf  38054  wl-euae  38059  wl-dfclab  38127  cnambfre  38206  triantru3  38774  lub0N  39852  glb0N  39856  cvlsupr3  40007  ifpdfor2  44078  ifpdfor  44082  ifpim1  44086  ifpid2  44088  ifpim2  44089  ifpid2g  44110  ifpid1g  44111  ifpim23g  44112  ifpim1g  44118  ifpimimb  44121  rp-isfinite6  44135  rababg  44191  relnonrel  44204  dffrege115  44595  chnsubseqwl  47486  funressnfv  47668  dfnelbr2  47898  edgusgrclnbfin  48495