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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  mpbiran  705  cases  1039  truan  1550  2sb5rf  2472  euae  2661  rexv  3447  reuv  3448  rmov  3449  rabab  3450  euxfrw  3651  euxfr  3653  euind  3654  dfdif3  4045  ddif  4067  nssinpss  4187  nsspssun  4188  notabw  4234  vss  4374  reuprg0  4635  reuprg  4636  difsnpss  4737  sspr  4763  sstp  4764  disjprgw  5065  disjprg  5066  mptv  5186  reusv2lem5  5320  oteqex2  5407  dfid4  5481  intirr  6012  xpcan  6068  resssxp  6162  fvopab6  6890  fnressn  7012  riotav  7217  mpov  7364  sorpss  7559  opabn1stprc  7871  fparlem2  7924  fnsuppres  7978  brtpos0  8020  sup0riota  9154  genpass  10696  nnwos  12584  hashbclem  14092  ccatlcan  14359  clim0  15143  gcd0id  16154  pjfval2  20826  mat1dimbas  21529  pmatcollpw2lem  21834  isbasis3g  22007  opnssneib  22174  ssidcn  22314  qtopcld  22772  mdegleb  25134  vieta1  25377  lgsne0  26388  axpasch  27212  0wlk  28381  0clwlk  28395  shlesb1i  29649  chnlei  29748  pjneli  29986  cvexchlem  30631  dmdbr5ati  30685  elimifd  30787  lmxrge0  31804  cntnevol  32096  bnj110  32738  goeleq12bg  33211  fmlafvel  33247  elpotr  33663  naddid1  33763  dfbigcup2  34128  bj-rexvw  34992  bj-rababw  34993  bj-brab2a1  35247  finxpreclem4  35492  wl-cases2-dnf  35598  wl-euae  35603  wl-dfclab  35674  cnambfre  35752  triantru3  36307  lub0N  37130  glb0N  37134  cvlsupr3  37285  isdomn3  40945  ifpdfor2  40966  ifpdfor  40970  ifpim1  40974  ifpid2  40976  ifpim2  40977  ifpid2g  40998  ifpid1g  40999  ifpim23g  41000  ifpim1g  41006  ifpimimb  41009  rp-isfinite6  41023  rababg  41070  relnonrel  41084  dffrege115  41475  funressnfv  44424  dfnelbr2  44652