Theorem biantrur 538

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpbiran  719  cases  1054  truan  1571  2sb5rf  2503  euae  2686  rexv  3481  reuv  3482  rmov  3483  rabab  3484  euxfrw  3684  euxfr  3686  euind  3687  dfdif3OLD  4072  ddif  4094  nssinpss  4219  nsspssun  4220  notabw  4265  vss  4400  reuprg0  4661  reuprg  4662  difsnpss  4767  sspr  4793  sstp  4794  disjprg  5096  mptv  5206  reusv2lem5  5359  oteqex2  5468  dfid4  5543  intirr  6105  xpcan  6162  resssxp  6257  fvopab6  7010  fnressn  7141  riotav  7358  mpov  7508  sorpss  7711  opabn1stprc  8039  fparlem2  8092  fnsuppres  8171  brtpos0  8213  naddrid  8654  sup0riota  9412  genpass  10967  nnwos  12916  hashbclem  14465  ccatlcan  14731  clim0  15533  gcd0id  16553  isdomn3  20765  pjfval2  21761  mat1dimbas  22532  pmatcollpw2lem  22837  isbasis3g  23009  opnssneib  23175  ssidcn  23315  qtopcld  23773  mdegleb  26124  vieta1  26376  lgsne0  27399  axpasch  29142  0wlk  30318  0clwlk  30332  shlesb1i  31589  chnlei  31688  pjneli  31926  cvexchlem  32571  dmdbr5ati  32625  elimifd  32742  fzo0opth  33005  1arithidom  33733  lmxrge0  34249  cntnevol  34525  bnj110  35153  vonf1wev  35451  vonf1owevOLD  35453  goeleq12bg  35699  fmlafvel  35735  elpotr  36129  dfbigcup2  36247  mh-regprimbi  36905  bj-alnnf  37212  bj-rexvw  37365  bj-rababw  37366  bj-brab2a1  37641  finxpreclem4  37888  wl-cases2-dnf  38015  wl-euae  38020  wl-dfclab  38088  cnambfre  38167  triantru3  38735  lub0N  39813  glb0N  39817  cvlsupr3  39968  ifpdfor2  44037  ifpdfor  44041  ifpim1  44045  ifpid2  44047  ifpim2  44048  ifpid2g  44069  ifpid1g  44070  ifpim23g  44071  ifpim1g  44077  ifpimimb  44080  rp-isfinite6  44094  rababg  44150  relnonrel  44163  dffrege115  44554  chnsubseqwl  47455  funressnfv  47637  dfnelbr2  47867  edgusgrclnbfin  48464