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  1580  2sb5rf  2501  euae  2684  rexv  3477  reuv  3478  rmov  3479  rabab  3480  euxfrw  3678  euxfr  3680  euind  3681  ddif  4076  nssinpss  4211  nsspssun  4212  notabw  4257  vss  4357  reuprg0  4659  reuprg  4660  difsnpss  4766  sspr  4789  sstp  4790  disjprg  5098  mptv  5210  reusv2lem5  5364  oteqex2  5471  dfid4  5547  intirr  6114  xpcan  6170  resssxp  6275  fvopab6  7033  fnressn  7167  riotav  7386  mpov  7536  mpt3fvd  7692  sorpss  7748  opabn1stprc  8074  fparlem2  8131  fnsuppres  8216  brtpos0  8258  naddrid  8701  sup0riota  9465  genpass  11101  nnwos  13049  hashbclem  14604  ccatlcan  14875  clim0  15682  gcd0id  16700  isdomn3  20975  pjfval2  22024  mat1dimbas  22796  pmatcollpw2lem  23104  isbasis3g  23276  opnssneib  23442  ssidcn  23582  qtopcld  24041  mdegleb  26391  vieta1  26644  lgsne0  27671  axpasch  29528  0wlk  30716  0clwlk  30730  shlesb1i  31997  chnlei  32096  pjneli  32334  cvexchlem  32979  dmdbr5ati  33033  elimifd  33190  fzo0opth  33445  1arithidom  34119  lmxrge0  34634  cntnevol  34911  bnj110  35538  vonf1wev  35987  vonf1owevOLD  35989  goeleq12bg  36232  fmlafvel  36268  elpotr  36667  dfbigcup2  36785  mh-regprimbi  37457  bj-alnnf  37763  bj-rexvw  37916  bj-rababw  37917  relpart  38088  bj-brab2a1  38207  finxpreclem4  38454  wl-cases2-dnf  38581  wl-euae  38586  wl-dfclab  38654  cnambfre  38723  triantru3  39305  lub0N  40383  glb0N  40387  cvlsupr3  40538  ifpdfor2  44599  ifpdfor  44603  ifpim1  44607  ifpid2  44609  ifpim2  44610  ifpid2g  44631  ifpid1g  44632  ifpim23g  44633  ifpim1g  44639  ifpimimb  44642  rp-isfinite6  44656  rababg  44712  relnonrel  44724  dffrege115  45115  chnsubseqwl  48025  funressnfv  48249  dfnelbr2  48479  edgusgrclnbfin  49076