Theorem biantrur 533

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

Syntax hints:   ↔ wb 208   ∧ wa 398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mpbiran  707  cases  1037  truan  1544  2sb5rf  2492  euae  2743  rexv  3520  reuv  3521  rmov  3522  rabab  3523  euxfrw  3711  euxfr  3713  euind  3714  dfdif3  4090  ddif  4112  nssinpss  4232  nsspssun  4233  vss  4394  reuprg0  4631  reuprg  4632  difsnpss  4733  sspr  4759  sstp  4760  disjprgw  5053  disjprg  5054  mptv  5163  reusv2lem5  5294  oteqex2  5381  dfid4  5455  intirr  5972  xpcan  6027  fvopab6  6795  fnressn  6914  riotav  7113  mpov  7258  sorpss  7448  opabn1stprc  7750  fparlem2  7802  fnsuppres  7851  brtpos0  7893  sup0riota  8923  genpass  10425  nnwos  12309  hashbclem  13804  ccatlcan  14074  clim0  14857  gcd0id  15861  pjfval2  20847  mat1dimbas  21075  pmatcollpw2lem  21379  isbasis3g  21551  opnssneib  21717  ssidcn  21857  qtopcld  22315  mdegleb  24652  vieta1  24895  lgsne0  25905  axpasch  26721  0wlk  27889  0clwlk  27903  shlesb1i  29157  chnlei  29256  pjneli  29494  cvexchlem  30139  dmdbr5ati  30193  elimifd  30292  lmxrge0  31190  cntnevol  31482  bnj110  32125  goeleq12bg  32591  fmlafvel  32627  elpotr  33021  dfbigcup2  33355  bj-rexvw  34191  bj-rababw  34192  bj-brab2a1  34435  finxpreclem4  34669  wl-cases2-dnf  34746  wl-euae  34751  wl-dfclab  34822  cnambfre  34934  triantru3  35494  lub0N  36319  glb0N  36323  cvlsupr3  36474  isdomn3  39797  ifpdfor2  39819  ifpdfor  39823  ifpim1  39827  ifpid2  39829  ifpim2  39830  ifpid2g  39852  ifpid1g  39853  ifpim23g  39854  ifpim1g  39860  ifpimimb  39863  rp-isfinite6  39877  rababg  39926  relnonrel  39940  rp-imass  40110  dffrege115  40317  funressnfv  43272  dfnelbr2  43466