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  710  cases  1043  truan  1553  2sb5rf  2477  euae  2661  rexv  3458  reuv  3459  rmov  3460  rabab  3461  euxfrw  3668  euxfr  3670  euind  3671  dfdif3OLD  4059  ddif  4082  nssinpss  4208  nsspssun  4209  notabw  4254  vss  4387  reuprg0  4647  reuprg  4648  difsnpss  4751  sspr  4779  sstp  4780  disjprg  5082  mptv  5192  reusv2lem5  5340  oteqex2  5448  dfid4  5521  intirr  6076  xpcan  6135  resssxp  6229  fvopab6  6977  fnressn  7106  riotav  7323  mpov  7473  sorpss  7676  opabn1stprc  8005  fparlem2  8057  fnsuppres  8135  brtpos0  8177  naddrid  8613  sup0riota  9373  genpass  10926  nnwos  12859  hashbclem  14408  ccatlcan  14674  clim0  15462  gcd0id  16482  isdomn3  20686  pjfval2  21702  mat1dimbas  22450  pmatcollpw2lem  22755  isbasis3g  22927  opnssneib  23093  ssidcn  23233  qtopcld  23691  mdegleb  26042  vieta1  26292  lgsne0  27315  axpasch  29027  0wlk  30204  0clwlk  30218  shlesb1i  31475  chnlei  31574  pjneli  31812  cvexchlem  32457  dmdbr5ati  32511  elimifd  32631  fzo0opth  32894  1arithidom  33615  lmxrge0  34115  cntnevol  34391  bnj110  35019  vonf1owev  35309  goeleq12bg  35550  fmlafvel  35586  elpotr  35980  dfbigcup2  36098  mh-regprimbi  36746  bj-alnnf  37053  bj-rexvw  37206  bj-rababw  37207  bj-brab2a1  37482  finxpreclem4  37727  wl-cases2-dnf  37854  wl-euae  37859  wl-dfclab  37927  cnambfre  38006  triantru3  38574  lub0N  39652  glb0N  39656  cvlsupr3  39807  ifpdfor2  43909  ifpdfor  43913  ifpim1  43917  ifpid2  43919  ifpim2  43920  ifpid2g  43941  ifpid1g  43942  ifpim23g  43943  ifpim1g  43949  ifpimimb  43952  rp-isfinite6  43966  rababg  44022  relnonrel  44035  dffrege115  44426  chnsubseqwl  47328  funressnfv  47506  dfnelbr2  47736  edgusgrclnbfin  48333