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  1551  2sb5rf  2470  euae  2653  rexv  3472  reuv  3473  rmov  3474  rabab  3475  euxfrw  3689  euxfr  3691  euind  3692  dfdif3OLD  4077  ddif  4100  nssinpss  4226  nsspssun  4227  notabw  4272  vss  4405  reuprg0  4662  reuprg  4663  difsnpss  4767  sspr  4795  sstp  4796  disjprg  5098  mptv  5208  reusv2lem5  5352  oteqex2  5454  dfid4  5527  intirr  6079  xpcan  6137  resssxp  6231  fvopab6  6984  fnressn  7112  riotav  7331  mpov  7481  sorpss  7684  opabn1stprc  8016  fparlem2  8069  fnsuppres  8147  brtpos0  8189  naddrid  8624  sup0riota  9393  genpass  10938  nnwos  12850  hashbclem  14393  ccatlcan  14659  clim0  15448  gcd0id  16465  isdomn3  20600  pjfval2  21594  mat1dimbas  22335  pmatcollpw2lem  22640  isbasis3g  22812  opnssneib  22978  ssidcn  23118  qtopcld  23576  mdegleb  25945  vieta1  26196  lgsne0  27222  axpasch  28844  0wlk  30018  0clwlk  30032  shlesb1i  31288  chnlei  31387  pjneli  31625  cvexchlem  32270  dmdbr5ati  32324  elimifd  32445  fzo0opth  32701  1arithidom  33481  lmxrge0  33915  cntnevol  34191  bnj110  34821  vonf1owev  35068  goeleq12bg  35309  fmlafvel  35345  elpotr  35742  dfbigcup2  35860  bj-rexvw  36841  bj-rababw  36842  bj-brab2a1  37110  finxpreclem4  37355  wl-cases2-dnf  37473  wl-euae  37478  wl-dfclab  37557  cnambfre  37635  triantru3  38191  lub0N  39155  glb0N  39159  cvlsupr3  39310  ifpdfor2  43423  ifpdfor  43427  ifpim1  43431  ifpid2  43433  ifpim2  43434  ifpid2g  43455  ifpid1g  43456  ifpim23g  43457  ifpim1g  43463  ifpimimb  43466  rp-isfinite6  43480  rababg  43536  relnonrel  43549  dffrege115  43940  funressnfv  47017  dfnelbr2  47247  edgusgrclnbfin  47815