Theorem biantrur 539

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpbiran  721  cases  1058  truan  1581  2sb5rf  2504  euae  2687  rexv  3482  reuv  3483  rmov  3484  rabab  3485  euxfrw  3684  euxfr  3686  euind  3687  dfdif3OLD  4073  ddif  4095  nssinpss  4220  nsspssun  4221  notabw  4266  vss  4365  reuprg0  4668  reuprg  4669  difsnpss  4775  sspr  4800  sstp  4801  disjprg  5105  mptv  5217  reusv2lem5  5373  oteqex2  5482  dfid4  5557  intirr  6118  xpcan  6174  resssxp  6271  fvopab6  7024  fnressn  7155  riotav  7372  mpov  7522  sorpss  7725  opabn1stprc  8051  fparlem2  8104  fnsuppres  8183  brtpos0  8225  naddrid  8666  sup0riota  9422  genpass  10989  nnwos  12934  hashbclem  14485  ccatlcan  14751  clim0  15553  gcd0id  16572  isdomn3  20813  pjfval2  21859  mat1dimbas  22629  pmatcollpw2lem  22934  isbasis3g  23106  opnssneib  23272  ssidcn  23412  qtopcld  23870  mdegleb  26221  vieta1  26473  lgsne0  27499  axpasch  29291  0wlk  30467  0clwlk  30481  shlesb1i  31738  chnlei  31837  pjneli  32075  cvexchlem  32720  dmdbr5ati  32774  elimifd  32889  fzo0opth  33148  1arithidom  33827  lmxrge0  34342  cntnevol  34618  bnj110  35246  vonf1wev  35592  vonf1owevOLD  35594  goeleq12bg  35841  fmlafvel  35877  elpotr  36271  dfbigcup2  36389  mh-regprimbi  37056  bj-alnnf  37362  bj-rexvw  37515  bj-rababw  37516  bj-brab2a1  37793  finxpreclem4  38040  wl-cases2-dnf  38167  wl-euae  38172  wl-dfclab  38240  cnambfre  38319  triantru3  38885  lub0N  39963  glb0N  39967  cvlsupr3  40118  ifpdfor2  44187  ifpdfor  44191  ifpim1  44195  ifpid2  44197  ifpim2  44198  ifpid2g  44219  ifpid1g  44220  ifpim23g  44221  ifpim1g  44227  ifpimimb  44230  rp-isfinite6  44244  rababg  44300  relnonrel  44313  dffrege115  44704  chnsubseqwl  47595  funressnfv  47780  dfnelbr2  48010  edgusgrclnbfin  48607