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  3475  reuv  3476  rmov  3477  rabab  3478  euxfrw  3692  euxfr  3694  euind  3695  dfdif3OLD  4081  ddif  4104  nssinpss  4230  nsspssun  4231  notabw  4276  vss  4409  reuprg0  4666  reuprg  4667  difsnpss  4771  sspr  4799  sstp  4800  disjprg  5103  mptv  5213  reusv2lem5  5357  oteqex2  5459  dfid4  5534  intirr  6091  xpcan  6149  resssxp  6243  fvopab6  7002  fnressn  7130  riotav  7349  mpov  7501  sorpss  7704  opabn1stprc  8037  fparlem2  8092  fnsuppres  8170  brtpos0  8212  naddrid  8647  sup0riota  9417  genpass  10962  nnwos  12874  hashbclem  14417  ccatlcan  14683  clim0  15472  gcd0id  16489  isdomn3  20624  pjfval2  21618  mat1dimbas  22359  pmatcollpw2lem  22664  isbasis3g  22836  opnssneib  23002  ssidcn  23142  qtopcld  23600  mdegleb  25969  vieta1  26220  lgsne0  27246  axpasch  28868  0wlk  30045  0clwlk  30059  shlesb1i  31315  chnlei  31414  pjneli  31652  cvexchlem  32297  dmdbr5ati  32351  elimifd  32472  fzo0opth  32728  1arithidom  33508  lmxrge0  33942  cntnevol  34218  bnj110  34848  vonf1owev  35095  goeleq12bg  35336  fmlafvel  35372  elpotr  35769  dfbigcup2  35887  bj-rexvw  36868  bj-rababw  36869  bj-brab2a1  37137  finxpreclem4  37382  wl-cases2-dnf  37500  wl-euae  37505  wl-dfclab  37584  cnambfre  37662  triantru3  38218  lub0N  39182  glb0N  39186  cvlsupr3  39337  ifpdfor2  43450  ifpdfor  43454  ifpim1  43458  ifpid2  43460  ifpim2  43461  ifpid2g  43482  ifpid1g  43483  ifpim23g  43484  ifpim1g  43490  ifpimimb  43493  rp-isfinite6  43507  rababg  43563  relnonrel  43576  dffrege115  43967  funressnfv  47044  dfnelbr2  47274  edgusgrclnbfin  47842