Theorem biantrur 531

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpbiran  706  cases  1040  truan  1550  2sb5rf  2473  euae  2662  rexv  3458  reuv  3459  rmov  3460  rabab  3461  euxfrw  3657  euxfr  3659  euind  3660  dfdif3  4050  ddif  4072  nssinpss  4191  nsspssun  4192  notabw  4238  vss  4378  reuprg0  4639  reuprg  4640  difsnpss  4741  sspr  4767  sstp  4768  disjprgw  5070  disjprg  5071  mptv  5191  reusv2lem5  5326  oteqex2  5414  dfid4  5491  intirr  6028  xpcan  6084  resssxp  6177  fvopab6  6917  fnressn  7039  riotav  7246  mpov  7395  sorpss  7590  opabn1stprc  7907  fparlem2  7962  fnsuppres  8016  brtpos0  8058  sup0riota  9233  genpass  10774  nnwos  12664  hashbclem  14173  ccatlcan  14440  clim0  15224  gcd0id  16235  pjfval2  20925  mat1dimbas  21630  pmatcollpw2lem  21935  isbasis3g  22108  opnssneib  22275  ssidcn  22415  qtopcld  22873  mdegleb  25238  vieta1  25481  lgsne0  26492  axpasch  27318  0wlk  28489  0clwlk  28503  shlesb1i  29757  chnlei  29856  pjneli  30094  cvexchlem  30739  dmdbr5ati  30793  elimifd  30895  lmxrge0  31911  cntnevol  32205  bnj110  32847  goeleq12bg  33320  fmlafvel  33356  elpotr  33766  naddid1  33845  dfbigcup2  34210  bj-rexvw  35074  bj-rababw  35075  bj-brab2a1  35329  finxpreclem4  35574  wl-cases2-dnf  35680  wl-euae  35685  wl-dfclab  35756  cnambfre  35834  triantru3  36389  lub0N  37210  glb0N  37214  cvlsupr3  37365  isdomn3  41036  ifpdfor2  41075  ifpdfor  41079  ifpim1  41083  ifpid2  41085  ifpim2  41086  ifpid2g  41107  ifpid1g  41108  ifpim23g  41109  ifpim1g  41115  ifpimimb  41118  rp-isfinite6  41132  rababg  41188  relnonrel  41202  dffrege115  41593  funressnfv  44548  dfnelbr2  44776