Theorem biantrur 535

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

Syntax hints:   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  mpbiran  715  cases  1048  truan  1558  2sb5rf  2480  euae  2663  rexv  3458  reuv  3459  rmov  3460  rabab  3461  euxfrw  3662  euxfr  3664  euind  3665  dfdif3OLD  4049  ddif  4071  nssinpss  4195  nsspssun  4196  notabw  4241  vss  4374  reuprg0  4634  reuprg  4635  difsnpss  4740  sspr  4766  sstp  4767  disjprg  5068  mptv  5178  reusv2lem5  5331  oteqex2  5440  dfid4  5514  intirr  6068  xpcan  6127  resssxp  6221  fvopab6  6970  fnressn  7101  riotav  7318  mpov  7468  sorpss  7671  opabn1stprc  8000  fparlem2  8052  fnsuppres  8131  brtpos0  8173  naddrid  8609  sup0riota  9369  genpass  10923  nnwos  12856  hashbclem  14405  ccatlcan  14671  clim0  15459  gcd0id  16479  isdomn3  20687  pjfval2  21684  mat1dimbas  22455  pmatcollpw2lem  22760  isbasis3g  22932  opnssneib  23098  ssidcn  23238  qtopcld  23696  mdegleb  26047  vieta1  26296  lgsne0  27316  axpasch  29028  0wlk  30204  0clwlk  30218  shlesb1i  31475  chnlei  31574  pjneli  31812  cvexchlem  32457  dmdbr5ati  32511  elimifd  32631  fzo0opth  32895  1arithidom  33620  lmxrge0  34136  cntnevol  34412  bnj110  35040  vonf1owev  35336  goeleq12bg  35577  fmlafvel  35613  elpotr  36007  dfbigcup2  36125  mh-regprimbi  36773  bj-alnnf  37080  bj-rexvw  37233  bj-rababw  37234  bj-brab2a1  37509  finxpreclem4  37756  wl-cases2-dnf  37883  wl-euae  37888  wl-dfclab  37956  cnambfre  38035  triantru3  38603  lub0N  39681  glb0N  39685  cvlsupr3  39836  ifpdfor2  43905  ifpdfor  43909  ifpim1  43913  ifpid2  43915  ifpim2  43916  ifpid2g  43937  ifpid1g  43938  ifpim23g  43939  ifpim1g  43945  ifpimimb  43948  rp-isfinite6  43962  rababg  44018  relnonrel  44031  dffrege115  44422  chnsubseqwl  47324  funressnfv  47506  dfnelbr2  47736  edgusgrclnbfin  48333