Theorem biantrur 531

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpbiran  707  cases  1041  truan  1552  2sb5rf  2470  euae  2654  rexv  3471  reuv  3472  rmov  3473  rabab  3474  euxfrw  3682  euxfr  3684  euind  3685  dfdif3  4079  ddif  4101  nssinpss  4221  nsspssun  4222  notabw  4268  vss  4408  reuprg0  4668  reuprg  4669  difsnpss  4772  sspr  4798  sstp  4799  disjprgw  5105  disjprg  5106  mptv  5226  reusv2lem5  5362  oteqex2  5461  dfid4  5537  intirr  6077  xpcan  6133  resssxp  6227  fvopab6  6986  fnressn  7109  riotav  7323  mpov  7473  sorpss  7670  opabn1stprc  7995  fparlem2  8050  fnsuppres  8127  brtpos0  8169  naddrid  8634  sup0riota  9410  genpass  10954  nnwos  12849  hashbclem  14361  ccatlcan  14618  clim0  15400  gcd0id  16410  pjfval2  21152  mat1dimbas  21858  pmatcollpw2lem  22163  isbasis3g  22336  opnssneib  22503  ssidcn  22643  qtopcld  23101  mdegleb  25466  vieta1  25709  lgsne0  26720  axpasch  27953  0wlk  29123  0clwlk  29137  shlesb1i  30391  chnlei  30490  pjneli  30728  cvexchlem  31373  dmdbr5ati  31427  elimifd  31529  lmxrge0  32622  cntnevol  32916  bnj110  33559  goeleq12bg  34030  fmlafvel  34066  elpotr  34442  dfbigcup2  34560  bj-rexvw  35423  bj-rababw  35424  bj-brab2a1  35693  finxpreclem4  35938  wl-cases2-dnf  36044  wl-euae  36049  wl-dfclab  36121  cnambfre  36199  triantru3  36758  lub0N  37724  glb0N  37728  cvlsupr3  37879  isdomn3  41589  ifpdfor2  41855  ifpdfor  41859  ifpim1  41863  ifpid2  41865  ifpim2  41866  ifpid2g  41887  ifpid1g  41888  ifpim23g  41889  ifpim1g  41895  ifpimimb  41898  rp-isfinite6  41912  rababg  41968  relnonrel  41981  dffrege115  42372  funressnfv  45397  dfnelbr2  45625