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  1550  2sb5rf  2476  euae  2659  rexv  3508  reuv  3509  rmov  3510  rabab  3511  euxfrw  3726  euxfr  3728  euind  3729  dfdif3OLD  4117  ddif  4140  nssinpss  4266  nsspssun  4267  notabw  4312  vss  4445  reuprg0  4701  reuprg  4702  difsnpss  4806  sspr  4834  sstp  4835  disjprg  5138  mptv  5257  reusv2lem5  5401  oteqex2  5503  dfid4  5578  intirr  6137  xpcan  6195  resssxp  6289  fvopab6  7049  fnressn  7177  riotav  7394  mpov  7546  sorpss  7749  opabn1stprc  8084  fparlem2  8139  fnsuppres  8217  brtpos0  8259  naddrid  8722  sup0riota  9506  genpass  11050  nnwos  12958  hashbclem  14492  ccatlcan  14757  clim0  15543  gcd0id  16557  isdomn3  20716  pjfval2  21730  mat1dimbas  22479  pmatcollpw2lem  22784  isbasis3g  22957  opnssneib  23124  ssidcn  23264  qtopcld  23722  mdegleb  26104  vieta1  26355  lgsne0  27380  axpasch  28957  0wlk  30136  0clwlk  30150  shlesb1i  31406  chnlei  31505  pjneli  31743  cvexchlem  32388  dmdbr5ati  32442  elimifd  32557  fzo0opth  32808  1arithidom  33566  lmxrge0  33952  cntnevol  34230  bnj110  34873  goeleq12bg  35355  fmlafvel  35391  elpotr  35783  dfbigcup2  35901  bj-rexvw  36882  bj-rababw  36883  bj-brab2a1  37151  finxpreclem4  37396  wl-cases2-dnf  37514  wl-euae  37519  wl-dfclab  37598  cnambfre  37676  triantru3  38232  lub0N  39191  glb0N  39195  cvlsupr3  39346  ifpdfor2  43479  ifpdfor  43483  ifpim1  43487  ifpid2  43489  ifpim2  43490  ifpid2g  43511  ifpid1g  43512  ifpim23g  43513  ifpim1g  43519  ifpimimb  43522  rp-isfinite6  43536  rababg  43592  relnonrel  43605  dffrege115  43996  funressnfv  47060  dfnelbr2  47290  edgusgrclnbfin  47833