Theorem biantrur 540

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpbiran  722  cases  1058  truan  1581  2sb5rf  2506  euae  2689  rexv  3484  reuv  3485  rmov  3486  rabab  3487  euxfrw  3686  euxfr  3688  euind  3689  ddif  4095  nssinpss  4220  nsspssun  4221  notabw  4266  vss  4365  reuprg0  4670  reuprg  4671  difsnpss  4777  sspr  4802  sstp  4803  disjprg  5107  mptv  5219  reusv2lem5  5375  oteqex2  5484  dfid4  5559  intirr  6120  xpcan  6176  resssxp  6274  fvopab6  7028  fnressn  7161  riotav  7381  mpov  7531  sorpss  7735  opabn1stprc  8061  fparlem2  8114  fnsuppres  8193  brtpos0  8235  naddrid  8676  sup0riota  9433  genpass  11009  nnwos  12955  hashbclem  14507  ccatlcan  14777  clim0  15581  gcd0id  16599  isdomn3  20863  pjfval2  21909  mat1dimbas  22679  pmatcollpw2lem  22984  isbasis3g  23156  opnssneib  23322  ssidcn  23462  qtopcld  23921  mdegleb  26272  vieta1  26524  lgsne0  27550  axpasch  29346  0wlk  30534  0clwlk  30548  shlesb1i  31809  chnlei  31908  pjneli  32146  cvexchlem  32791  dmdbr5ati  32845  elimifd  32960  fzo0opth  33218  1arithidom  33891  lmxrge0  34406  cntnevol  34683  bnj110  35311  vonf1wev  35649  vonf1owevOLD  35651  goeleq12bg  35878  fmlafvel  35914  elpotr  36308  dfbigcup2  36426  mh-regprimbi  37113  bj-alnnf  37419  bj-rexvw  37572  bj-rababw  37573  bj-brab2a1  37850  finxpreclem4  38097  wl-cases2-dnf  38224  wl-euae  38229  wl-dfclab  38297  cnambfre  38376  triantru3  38943  lub0N  40021  glb0N  40025  cvlsupr3  40176  ifpdfor2  44245  ifpdfor  44249  ifpim1  44253  ifpid2  44255  ifpim2  44256  ifpid2g  44277  ifpid1g  44278  ifpim23g  44279  ifpim1g  44285  ifpimimb  44288  rp-isfinite6  44302  rababg  44358  relnonrel  44371  dffrege115  44762  chnsubseqwl  47653  funressnfv  47838  dfnelbr2  48068  edgusgrclnbfin  48665