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  1552  2sb5rf  2474  euae  2658  rexv  3466  reuv  3467  rmov  3468  rabab  3469  euxfrw  3677  euxfr  3679  euind  3680  dfdif3OLD  4068  ddif  4091  nssinpss  4217  nsspssun  4218  notabw  4263  vss  4396  reuprg0  4657  reuprg  4658  difsnpss  4761  sspr  4789  sstp  4790  disjprg  5092  mptv  5202  reusv2lem5  5345  oteqex2  5445  dfid4  5518  intirr  6073  xpcan  6132  resssxp  6226  fvopab6  6973  fnressn  7101  riotav  7318  mpov  7468  sorpss  7671  opabn1stprc  8000  fparlem2  8053  fnsuppres  8131  brtpos0  8173  naddrid  8609  sup0riota  9367  genpass  10918  nnwos  12826  hashbclem  14373  ccatlcan  14639  clim0  15427  gcd0id  16444  isdomn3  20646  pjfval2  21662  mat1dimbas  22414  pmatcollpw2lem  22719  isbasis3g  22891  opnssneib  23057  ssidcn  23197  qtopcld  23655  mdegleb  26023  vieta1  26274  lgsne0  27300  axpasch  28963  0wlk  30140  0clwlk  30154  shlesb1i  31410  chnlei  31509  pjneli  31747  cvexchlem  32392  dmdbr5ati  32446  elimifd  32567  fzo0opth  32832  1arithidom  33567  lmxrge0  34058  cntnevol  34334  bnj110  34963  vonf1owev  35251  goeleq12bg  35492  fmlafvel  35528  elpotr  35922  dfbigcup2  36040  bj-rexvw  37024  bj-rababw  37025  bj-brab2a1  37293  finxpreclem4  37538  wl-cases2-dnf  37656  wl-euae  37661  wl-dfclab  37729  cnambfre  37808  triantru3  38371  lub0N  39388  glb0N  39392  cvlsupr3  39543  ifpdfor2  43644  ifpdfor  43648  ifpim1  43652  ifpid2  43654  ifpim2  43655  ifpid2g  43676  ifpid1g  43677  ifpim23g  43678  ifpim1g  43684  ifpimimb  43687  rp-isfinite6  43701  rababg  43757  relnonrel  43770  dffrege115  44161  chnsubseqwl  47065  funressnfv  47231  dfnelbr2  47461  edgusgrclnbfin  48030