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  2504  euae  2687  rexv  3481  reuv  3482  rmov  3483  rabab  3484  euxfrw  3682  euxfr  3684  euind  3685  ddif  4080  nssinpss  4215  nsspssun  4216  notabw  4261  vss  4361  reuprg0  4664  reuprg  4665  difsnpss  4772  sspr  4795  sstp  4796  disjprg  5104  mptv  5217  reusv2lem5  5371  oteqex2  5478  dfid4  5554  intirr  6130  xpcan  6186  resssxp  6296  fvopab6  7059  fnressn  7194  riotav  7413  mpov  7563  mpt3fvd  7720  sorpss  7776  opabn1stprc  8104  fparlem2  8161  fnsuppres  8246  brtpos0  8288  naddrid  8731  sup0riota  9495  genpass  11133  nnwos  13082  hashbclem  14638  ccatlcan  14909  clim0  15717  gcd0id  16735  isdomn3  21017  pjfval2  22070  mat1dimbas  22842  pmatcollpw2lem  23150  isbasis3g  23322  opnssneib  23488  ssidcn  23628  qtopcld  24087  mdegleb  26437  vieta1  26690  lgsne0  27719  axpasch  29576  0wlk  30764  0clwlk  30778  shlesb1i  32045  chnlei  32144  pjneli  32382  cvexchlem  33027  dmdbr5ati  33081  elimifd  33237  fzo0opth  33491  1arithidom  34173  lmxrge0  34695  cntnevol  34972  bnj110  35599  mpofvd  35838  vonf1wev  36077  vonf1owevOLD  36079  goeleq12bg  36322  fmlafvel  36358  elpotr  36758  dfbigcup2  36876  mh-regprimbi  37548  bj-alnnf  37854  bj-rexvw  38007  bj-rababw  38008  relpart  38186  bj-brab2a1  38338  finxpreclem4  38585  wl-cases2-dnf  38712  wl-euae  38717  wl-dfclab  38785  cnambfre  38854  triantru3  39434  lub0N  40512  glb0N  40516  cvlsupr3  40667  ifpdfor2  44723  ifpdfor  44727  ifpim1  44731  ifpid2  44733  ifpim2  44734  ifpid2g  44755  ifpid1g  44756  ifpim23g  44757  ifpim1g  44763  ifpimimb  44766  rp-isfinite6  44780  rababg  44836  relnonrel  44848  dffrege115  45239  chnsubseqwl  48162  funressnfv  48386  dfnelbr2  48616  edgusgrclnbfin  49213