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  2477  euae  2660  rexv  3493  reuv  3494  rmov  3495  rabab  3496  euxfrw  3709  euxfr  3711  euind  3712  dfdif3OLD  4098  ddif  4121  nssinpss  4247  nsspssun  4248  notabw  4293  vss  4426  reuprg0  4683  reuprg  4684  difsnpss  4788  sspr  4816  sstp  4817  disjprg  5120  mptv  5233  reusv2lem5  5377  oteqex2  5479  dfid4  5554  intirr  6112  xpcan  6170  resssxp  6264  fvopab6  7025  fnressn  7153  riotav  7372  mpov  7524  sorpss  7727  opabn1stprc  8062  fparlem2  8117  fnsuppres  8195  brtpos0  8237  naddrid  8700  sup0riota  9483  genpass  11028  nnwos  12936  hashbclem  14475  ccatlcan  14741  clim0  15527  gcd0id  16543  isdomn3  20680  pjfval2  21674  mat1dimbas  22415  pmatcollpw2lem  22720  isbasis3g  22892  opnssneib  23058  ssidcn  23198  qtopcld  23656  mdegleb  26026  vieta1  26277  lgsne0  27303  axpasch  28925  0wlk  30102  0clwlk  30116  shlesb1i  31372  chnlei  31471  pjneli  31709  cvexchlem  32354  dmdbr5ati  32408  elimifd  32529  fzo0opth  32787  1arithidom  33557  lmxrge0  33988  cntnevol  34264  bnj110  34894  goeleq12bg  35376  fmlafvel  35412  elpotr  35804  dfbigcup2  35922  bj-rexvw  36903  bj-rababw  36904  bj-brab2a1  37172  finxpreclem4  37417  wl-cases2-dnf  37535  wl-euae  37540  wl-dfclab  37619  cnambfre  37697  triantru3  38253  lub0N  39212  glb0N  39216  cvlsupr3  39367  ifpdfor2  43460  ifpdfor  43464  ifpim1  43468  ifpid2  43470  ifpim2  43471  ifpid2g  43492  ifpid1g  43493  ifpim23g  43494  ifpim1g  43500  ifpimimb  43503  rp-isfinite6  43517  rababg  43573  relnonrel  43586  dffrege115  43977  funressnfv  47052  dfnelbr2  47282  edgusgrclnbfin  47835