Theorem biantrur 523

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	. 2 ⊢ 𝜑
2		ibar 521	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  mpbiran  696  cases  1023  truan  1518  2sb5rf  2416  euae  2686  rexv  3435  reuv  3436  rmov  3437  rabab  3438  euxfr  3622  euind  3623  dfdif3  3977  ddif  3999  nssinpss  4115  nsspssun  4116  vss  4272  reuprg0  4506  reuprg  4507  difsnpss  4608  sspr  4634  sstp  4635  disjprg  4919  mptv  5023  reusv2lem5  5150  oteqex2  5238  dfid4  5307  intirr  5812  xpcan  5867  fvopab6  6620  fnressn  6737  riotav  6936  mpov  7074  sorpss  7266  opabn1stprc  7557  fparlem2  7609  fnsuppres  7653  brtpos0  7695  sup0riota  8716  genpass  10221  nnwos  12122  hashbclem  13613  ccatlcan  13900  clim0  14714  gcd0id  15717  pjfval2  20545  mat1dimbas  20775  pmatcollpw2lem  21079  isbasis3g  21251  opnssneib  21417  ssidcn  21557  qtopcld  22015  mdegleb  24351  vieta1  24594  lgsne0  25603  axpasch  26420  0wlk  27635  0clwlk  27649  shlesb1i  28934  chnlei  29033  pjneli  29271  cvexchlem  29916  dmdbr5ati  29970  elimifd  30056  lmxrge0  30796  cntnevol  31089  bnj110  31738  elpotr  32486  dfbigcup2  32821  bj-rexvw  33629  bj-rababw  33630  finxpreclem4  34051  wl-cases2-dnf  34128  wl-euae  34133  wl-dfclab  34217  cnambfre  34329  triantru3  34892  lub0N  35718  glb0N  35722  cvlsupr3  35873  isdomn3  39145  ifpdfor2  39167  ifpdfor  39171  ifpim1  39175  ifpid2  39177  ifpim2  39178  ifpid2g  39200  ifpid1g  39201  ifpim23g  39202  ifpim1g  39208  ifpimimb  39211  rp-isfinite6  39225  rababg  39240  relnonrel  39254  rp-imass  39425  dffrege115  39632  funressnfv  42629  dfnelbr2  42824