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  1548  2sb5rf  2475  euae  2658  rexv  3507  reuv  3508  rmov  3509  rabab  3510  euxfrw  3730  euxfr  3732  euind  3733  dfdif3OLD  4128  ddif  4151  nssinpss  4273  nsspssun  4274  notabw  4319  vss  4452  reuprg0  4707  reuprg  4708  difsnpss  4812  sspr  4840  sstp  4841  disjprg  5144  mptv  5264  reusv2lem5  5408  oteqex2  5509  dfid4  5584  intirr  6141  xpcan  6198  resssxp  6292  fvopab6  7050  fnressn  7178  riotav  7393  mpov  7545  sorpss  7747  opabn1stprc  8082  fparlem2  8137  fnsuppres  8215  brtpos0  8257  naddrid  8720  sup0riota  9503  genpass  11047  nnwos  12955  hashbclem  14488  ccatlcan  14753  clim0  15539  gcd0id  16553  isdomn3  20732  pjfval2  21747  mat1dimbas  22494  pmatcollpw2lem  22799  isbasis3g  22972  opnssneib  23139  ssidcn  23279  qtopcld  23737  mdegleb  26118  vieta1  26369  lgsne0  27394  axpasch  28971  0wlk  30145  0clwlk  30159  shlesb1i  31415  chnlei  31514  pjneli  31752  cvexchlem  32397  dmdbr5ati  32451  elimifd  32564  fzo0opth  32813  1arithidom  33545  lmxrge0  33913  cntnevol  34209  bnj110  34851  goeleq12bg  35334  fmlafvel  35370  elpotr  35763  dfbigcup2  35881  bj-rexvw  36863  bj-rababw  36864  bj-brab2a1  37132  finxpreclem4  37377  wl-cases2-dnf  37493  wl-euae  37498  wl-dfclab  37577  cnambfre  37655  triantru3  38211  lub0N  39171  glb0N  39175  cvlsupr3  39326  ifpdfor2  43451  ifpdfor  43455  ifpim1  43459  ifpid2  43461  ifpim2  43462  ifpid2g  43483  ifpid1g  43484  ifpim23g  43485  ifpim1g  43491  ifpimimb  43494  rp-isfinite6  43508  rababg  43564  relnonrel  43577  dffrege115  43968  funressnfv  46993  dfnelbr2  47223  edgusgrclnbfin  47766