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  1552  2sb5rf  2472  euae  2655  rexv  3464  reuv  3465  rmov  3466  rabab  3467  euxfrw  3675  euxfr  3677  euind  3678  dfdif3OLD  4065  ddif  4088  nssinpss  4214  nsspssun  4215  notabw  4260  vss  4393  reuprg0  4652  reuprg  4653  difsnpss  4756  sspr  4784  sstp  4785  disjprg  5085  mptv  5195  reusv2lem5  5338  oteqex2  5437  dfid4  5510  intirr  6064  xpcan  6123  resssxp  6217  fvopab6  6963  fnressn  7091  riotav  7308  mpov  7458  sorpss  7661  opabn1stprc  7990  fparlem2  8043  fnsuppres  8121  brtpos0  8163  naddrid  8598  sup0riota  9350  genpass  10900  nnwos  12813  hashbclem  14359  ccatlcan  14625  clim0  15413  gcd0id  16430  isdomn3  20630  pjfval2  21646  mat1dimbas  22387  pmatcollpw2lem  22692  isbasis3g  22864  opnssneib  23030  ssidcn  23170  qtopcld  23628  mdegleb  25996  vieta1  26247  lgsne0  27273  axpasch  28919  0wlk  30096  0clwlk  30110  shlesb1i  31366  chnlei  31465  pjneli  31703  cvexchlem  32348  dmdbr5ati  32402  elimifd  32523  fzo0opth  32785  1arithidom  33502  lmxrge0  33965  cntnevol  34241  bnj110  34870  vonf1owev  35152  goeleq12bg  35393  fmlafvel  35429  elpotr  35823  dfbigcup2  35941  bj-rexvw  36924  bj-rababw  36925  bj-brab2a1  37193  finxpreclem4  37438  wl-cases2-dnf  37556  wl-euae  37561  wl-dfclab  37640  cnambfre  37718  triantru3  38281  lub0N  39298  glb0N  39302  cvlsupr3  39453  ifpdfor2  43564  ifpdfor  43568  ifpim1  43572  ifpid2  43574  ifpim2  43575  ifpid2g  43596  ifpid1g  43597  ifpim23g  43598  ifpim1g  43604  ifpimimb  43607  rp-isfinite6  43621  rababg  43677  relnonrel  43690  dffrege115  44081  chnsubseqwl  46987  funressnfv  47153  dfnelbr2  47383  edgusgrclnbfin  47952