Theorem biantrur 533

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpbiran  707  cases  1037  truan  1548  2sb5rf  2496  euae  2745  rexv  3520  reuv  3521  rmov  3522  rabab  3523  euxfrw  3712  euxfr  3714  euind  3715  dfdif3  4091  ddif  4113  nssinpss  4233  nsspssun  4234  vss  4395  reuprg0  4638  reuprg  4639  difsnpss  4740  sspr  4766  sstp  4767  disjprgw  5061  disjprg  5062  mptv  5171  reusv2lem5  5303  oteqex2  5389  dfid4  5461  intirr  5978  xpcan  6033  fvopab6  6801  fnressn  6920  riotav  7119  mpov  7264  sorpss  7454  opabn1stprc  7756  fparlem2  7808  fnsuppres  7857  brtpos0  7899  sup0riota  8929  genpass  10431  nnwos  12316  hashbclem  13811  ccatlcan  14080  clim0  14863  gcd0id  15867  pjfval2  20853  mat1dimbas  21081  pmatcollpw2lem  21385  isbasis3g  21557  opnssneib  21723  ssidcn  21863  qtopcld  22321  mdegleb  24658  vieta1  24901  lgsne0  25911  axpasch  26727  0wlk  27895  0clwlk  27909  shlesb1i  29163  chnlei  29262  pjneli  29500  cvexchlem  30145  dmdbr5ati  30199  elimifd  30298  lmxrge0  31195  cntnevol  31487  bnj110  32130  goeleq12bg  32596  fmlafvel  32632  elpotr  33026  dfbigcup2  33360  bj-rexvw  34199  bj-rababw  34200  bj-brab2a1  34444  finxpreclem4  34678  wl-cases2-dnf  34767  wl-euae  34772  wl-dfclab  34843  cnambfre  34955  triantru3  35515  lub0N  36340  glb0N  36344  cvlsupr3  36495  isdomn3  39824  ifpdfor2  39846  ifpdfor  39850  ifpim1  39854  ifpid2  39856  ifpim2  39857  ifpid2g  39879  ifpid1g  39880  ifpim23g  39881  ifpim1g  39887  ifpimimb  39890  rp-isfinite6  39904  rababg  39953  relnonrel  39967  rp-imass  40137  dffrege115  40344  funressnfv  43298  dfnelbr2  43492