Theorem biantrur 530

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpbiran  709  cases  1042  truan  1551  2sb5rf  2470  euae  2653  rexv  3464  reuv  3465  rmov  3466  rabab  3467  euxfrw  3681  euxfr  3683  euind  3684  dfdif3OLD  4069  ddif  4092  nssinpss  4218  nsspssun  4219  notabw  4264  vss  4397  reuprg0  4654  reuprg  4655  difsnpss  4758  sspr  4786  sstp  4787  disjprg  5088  mptv  5198  reusv2lem5  5341  oteqex2  5442  dfid4  5515  intirr  6067  xpcan  6125  resssxp  6218  fvopab6  6964  fnressn  7092  riotav  7311  mpov  7461  sorpss  7664  opabn1stprc  7993  fparlem2  8046  fnsuppres  8124  brtpos0  8166  naddrid  8601  sup0riota  9356  genpass  10903  nnwos  12816  hashbclem  14359  ccatlcan  14624  clim0  15413  gcd0id  16430  isdomn3  20600  pjfval2  21616  mat1dimbas  22357  pmatcollpw2lem  22662  isbasis3g  22834  opnssneib  23000  ssidcn  23140  qtopcld  23598  mdegleb  25967  vieta1  26218  lgsne0  27244  axpasch  28886  0wlk  30060  0clwlk  30074  shlesb1i  31330  chnlei  31429  pjneli  31667  cvexchlem  32312  dmdbr5ati  32366  elimifd  32487  fzo0opth  32748  1arithidom  33474  lmxrge0  33919  cntnevol  34195  bnj110  34825  vonf1owev  35085  goeleq12bg  35326  fmlafvel  35362  elpotr  35759  dfbigcup2  35877  bj-rexvw  36858  bj-rababw  36859  bj-brab2a1  37127  finxpreclem4  37372  wl-cases2-dnf  37490  wl-euae  37495  wl-dfclab  37574  cnambfre  37652  triantru3  38208  lub0N  39172  glb0N  39176  cvlsupr3  39327  ifpdfor2  43438  ifpdfor  43442  ifpim1  43446  ifpid2  43448  ifpim2  43449  ifpid2g  43470  ifpid1g  43471  ifpim23g  43472  ifpim1g  43478  ifpimimb  43481  rp-isfinite6  43495  rababg  43551  relnonrel  43564  dffrege115  43955  funressnfv  47031  dfnelbr2  47261  edgusgrclnbfin  47830