Theorem biantrur 540

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpbiran  722  cases  1058  truan  1581  2sb5rf  2501  euae  2684  rexv  3477  reuv  3478  rmov  3479  rabab  3480  euxfrw  3679  euxfr  3681  euind  3682  ddif  4088  nssinpss  4213  nsspssun  4214  notabw  4259  vss  4358  reuprg0  4663  reuprg  4664  difsnpss  4770  sspr  4795  sstp  4796  disjprg  5099  mptv  5211  reusv2lem5  5367  oteqex2  5476  dfid4  5551  intirr  6112  xpcan  6169  resssxp  6267  fvopab6  7021  fnressn  7155  riotav  7375  mpov  7525  sorpss  7729  opabn1stprc  8055  fparlem2  8110  fnsuppres  8189  brtpos0  8231  naddrid  8672  sup0riota  9436  genpass  11018  nnwos  12964  hashbclem  14517  ccatlcan  14787  clim0  15593  gcd0id  16609  isdomn3  20876  pjfval2  21922  mat1dimbas  22694  pmatcollpw2lem  23002  isbasis3g  23174  opnssneib  23340  ssidcn  23480  qtopcld  23939  mdegleb  26289  vieta1  26544  lgsne0  27571  axpasch  29398  0wlk  30586  0clwlk  30600  shlesb1i  31867  chnlei  31966  pjneli  32204  cvexchlem  32849  dmdbr5ati  32903  elimifd  33018  fzo0opth  33274  1arithidom  33947  lmxrge0  34462  cntnevol  34739  bnj110  35367  vonf1wev  35705  vonf1owevOLD  35707  goeleq12bg  35928  fmlafvel  35964  elpotr  36358  dfbigcup2  36476  mh-regprimbi  37164  bj-alnnf  37470  bj-rexvw  37623  bj-rababw  37624  bj-brab2a1  37901  finxpreclem4  38148  wl-cases2-dnf  38275  wl-euae  38280  wl-dfclab  38348  cnambfre  38417  triantru3  38984  lub0N  40062  glb0N  40066  cvlsupr3  40217  ifpdfor2  44301  ifpdfor  44305  ifpim1  44309  ifpid2  44311  ifpim2  44312  ifpid2g  44333  ifpid1g  44334  ifpim23g  44335  ifpim1g  44341  ifpimimb  44344  rp-isfinite6  44358  rababg  44414  relnonrel  44427  dffrege115  44818  chnsubseqwl  47707  funressnfv  47931  dfnelbr2  48161  edgusgrclnbfin  48758