Theorem biantrur 529

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  mpbiran  705  cases  1039  truan  1550  2sb5rf  2469  euae  2653  rexv  3498  reuv  3499  rmov  3500  rabab  3501  euxfrw  3716  euxfr  3718  euind  3719  dfdif3  4113  ddif  4135  nssinpss  4255  nsspssun  4256  notabw  4302  vss  4442  reuprg0  4705  reuprg  4706  difsnpss  4809  sspr  4835  sstp  4836  disjprgw  5142  disjprg  5143  mptv  5263  reusv2lem5  5399  oteqex2  5498  dfid4  5574  intirr  6118  xpcan  6174  resssxp  6268  fvopab6  7030  fnressn  7157  riotav  7372  mpov  7522  sorpss  7720  opabn1stprc  8046  fparlem2  8101  fnsuppres  8178  brtpos0  8220  naddrid  8684  sup0riota  9462  genpass  11006  nnwos  12903  hashbclem  14415  ccatlcan  14672  clim0  15454  gcd0id  16464  pjfval2  21483  mat1dimbas  22194  pmatcollpw2lem  22499  isbasis3g  22672  opnssneib  22839  ssidcn  22979  qtopcld  23437  mdegleb  25817  vieta1  26061  lgsne0  27074  axpasch  28466  0wlk  29636  0clwlk  29650  shlesb1i  30906  chnlei  31005  pjneli  31243  cvexchlem  31888  dmdbr5ati  31942  elimifd  32042  lmxrge0  33230  cntnevol  33524  bnj110  34167  goeleq12bg  34638  fmlafvel  34674  elpotr  35057  dfbigcup2  35175  bj-rexvw  36063  bj-rababw  36064  bj-brab2a1  36333  finxpreclem4  36578  wl-cases2-dnf  36684  wl-euae  36689  wl-dfclab  36761  cnambfre  36839  triantru3  37397  lub0N  38362  glb0N  38366  cvlsupr3  38517  isdomn3  42248  ifpdfor2  42514  ifpdfor  42518  ifpim1  42522  ifpid2  42524  ifpim2  42525  ifpid2g  42546  ifpid1g  42547  ifpim23g  42548  ifpim1g  42554  ifpimimb  42557  rp-isfinite6  42571  rababg  42627  relnonrel  42640  dffrege115  43031  funressnfv  46051  dfnelbr2  46279