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  2502  euae  2685  rexv  3478  reuv  3479  rmov  3480  rabab  3481  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  5364  oteqex2  5471  dfid4  5547  intirr  6112  xpcan  6168  resssxp  6272  fvopab6  7028  fnressn  7162  riotav  7382  mpov  7532  mpt3fvd  7688  sorpss  7744  opabn1stprc  8069  fparlem2  8124  fnsuppres  8208  brtpos0  8250  naddrid  8693  sup0riota  9458  genpass  11094  nnwos  13042  hashbclem  14597  ccatlcan  14867  clim0  15673  gcd0id  16691  isdomn3  20966  pjfval2  22015  mat1dimbas  22787  pmatcollpw2lem  23095  isbasis3g  23267  opnssneib  23433  ssidcn  23573  qtopcld  24032  mdegleb  26382  vieta1  26635  lgsne0  27662  axpasch  29519  0wlk  30707  0clwlk  30721  shlesb1i  31988  chnlei  32087  pjneli  32325  cvexchlem  32970  dmdbr5ati  33024  elimifd  33139  fzo0opth  33395  1arithidom  34069  lmxrge0  34584  cntnevol  34861  bnj110  35488  vonf1wev  35887  vonf1owevOLD  35889  goeleq12bg  36114  fmlafvel  36150  elpotr  36543  dfbigcup2  36661  mh-regprimbi  37333  bj-alnnf  37639  bj-rexvw  37792  bj-rababw  37793  bj-brab2a1  38070  finxpreclem4  38317  wl-cases2-dnf  38444  wl-euae  38449  wl-dfclab  38517  cnambfre  38586  triantru3  39168  lub0N  40246  glb0N  40250  cvlsupr3  40401  ifpdfor2  44461  ifpdfor  44465  ifpim1  44469  ifpid2  44471  ifpim2  44472  ifpid2g  44493  ifpid1g  44494  ifpim23g  44495  ifpim1g  44501  ifpimimb  44504  rp-isfinite6  44518  rababg  44574  relnonrel  44586  dffrege115  44977  chnsubseqwl  47888  funressnfv  48112  dfnelbr2  48342  edgusgrclnbfin  48939