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  2501  euae  2684  rexv  3477  reuv  3478  rmov  3479  rabab  3480  euxfrw  3679  euxfr  3681  euind  3682  ddif  4088  nssinpss  4213  nsspssun  4214  notabw  4259  vss  4358  reuprg0  4663  reuprg  4664  difsnpss  4770  sspr  4795  sstp  4796  disjprg  5099  mptv  5211  reusv2lem5  5367  oteqex2  5476  dfid4  5551  intirr  6112  xpcan  6169  resssxp  6267  fvopab6  7022  fnressn  7156  riotav  7376  mpov  7526  sorpss  7730  opabn1stprc  8056  fparlem2  8111  fnsuppres  8190  brtpos0  8232  naddrid  8673  sup0riota  9437  genpass  11019  nnwos  12965  hashbclem  14518  ccatlcan  14788  clim0  15594  gcd0id  16610  isdomn3  20877  pjfval2  21923  mat1dimbas  22695  pmatcollpw2lem  23003  isbasis3g  23175  opnssneib  23341  ssidcn  23481  qtopcld  23940  mdegleb  26290  vieta1  26545  lgsne0  27572  axpasch  29399  0wlk  30587  0clwlk  30601  shlesb1i  31868  chnlei  31967  pjneli  32205  cvexchlem  32850  dmdbr5ati  32904  elimifd  33019  fzo0opth  33275  1arithidom  33948  lmxrge0  34463  cntnevol  34740  bnj110  35368  vonf1wev  35706  vonf1owevOLD  35708  goeleq12bg  35929  fmlafvel  35965  elpotr  36359  dfbigcup2  36477  mh-regprimbi  37165  bj-alnnf  37471  bj-rexvw  37624  bj-rababw  37625  bj-brab2a1  37902  finxpreclem4  38149  wl-cases2-dnf  38276  wl-euae  38281  wl-dfclab  38349  cnambfre  38418  triantru3  38985  lub0N  40063  glb0N  40067  cvlsupr3  40218  ifpdfor2  44302  ifpdfor  44306  ifpim1  44310  ifpid2  44312  ifpim2  44313  ifpid2g  44334  ifpid1g  44335  ifpim23g  44336  ifpim1g  44342  ifpimimb  44345  rp-isfinite6  44359  rababg  44415  relnonrel  44428  dffrege115  44819  chnsubseqwl  47708  funressnfv  47932  dfnelbr2  48162  edgusgrclnbfin  48759