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  710  cases  1043  truan  1553  2sb5rf  2476  euae  2660  rexv  3457  reuv  3458  rmov  3459  rabab  3460  euxfrw  3667  euxfr  3669  euind  3670  dfdif3OLD  4058  ddif  4081  nssinpss  4207  nsspssun  4208  notabw  4253  vss  4386  reuprg0  4646  reuprg  4647  difsnpss  4752  sspr  4778  sstp  4779  disjprg  5081  mptv  5191  reusv2lem5  5344  oteqex2  5453  dfid4  5527  intirr  6081  xpcan  6140  resssxp  6234  fvopab6  6982  fnressn  7112  riotav  7329  mpov  7479  sorpss  7682  opabn1stprc  8011  fparlem2  8063  fnsuppres  8141  brtpos0  8183  naddrid  8619  sup0riota  9379  genpass  10932  nnwos  12865  hashbclem  14414  ccatlcan  14680  clim0  15468  gcd0id  16488  isdomn3  20692  pjfval2  21689  mat1dimbas  22437  pmatcollpw2lem  22742  isbasis3g  22914  opnssneib  23080  ssidcn  23220  qtopcld  23678  mdegleb  26029  vieta1  26278  lgsne0  27298  axpasch  29010  0wlk  30186  0clwlk  30200  shlesb1i  31457  chnlei  31556  pjneli  31794  cvexchlem  32439  dmdbr5ati  32493  elimifd  32613  fzo0opth  32876  1arithidom  33597  lmxrge0  34096  cntnevol  34372  bnj110  35000  vonf1owev  35290  goeleq12bg  35531  fmlafvel  35567  elpotr  35961  dfbigcup2  36079  mh-regprimbi  36727  bj-alnnf  37034  bj-rexvw  37187  bj-rababw  37188  bj-brab2a1  37463  finxpreclem4  37710  wl-cases2-dnf  37837  wl-euae  37842  wl-dfclab  37910  cnambfre  37989  triantru3  38557  lub0N  39635  glb0N  39639  cvlsupr3  39790  ifpdfor2  43888  ifpdfor  43892  ifpim1  43896  ifpid2  43898  ifpim2  43899  ifpid2g  43920  ifpid1g  43921  ifpim23g  43922  ifpim1g  43928  ifpimimb  43931  rp-isfinite6  43945  rababg  44001  relnonrel  44014  dffrege115  44405  chnsubseqwl  47309  funressnfv  47491  dfnelbr2  47721  edgusgrclnbfin  48318