Theorem biantrur 534

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

Syntax hints:   ↔ wb 209   ∧ 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 210  df-an 400

This theorem is referenced by:  mpbiran  709  cases  1043  truan  1554  2sb5rf  2471  euae  2660  rexv  3423  reuv  3424  rmov  3425  rabab  3426  euxfrw  3623  euxfr  3625  euind  3626  dfdif3  4015  ddif  4037  nssinpss  4157  nsspssun  4158  notabw  4204  vss  4344  reuprg0  4604  reuprg  4605  difsnpss  4706  sspr  4732  sstp  4733  disjprgw  5034  disjprg  5035  mptv  5145  reusv2lem5  5280  oteqex2  5367  dfid4  5441  intirr  5963  xpcan  6019  resssxp  6113  fvopab6  6829  fnressn  6951  riotav  7153  mpov  7300  sorpss  7494  opabn1stprc  7806  fparlem2  7859  fnsuppres  7911  brtpos0  7953  sup0riota  9059  genpass  10588  nnwos  12476  hashbclem  13981  ccatlcan  14248  clim0  15032  gcd0id  16041  pjfval2  20625  mat1dimbas  21323  pmatcollpw2lem  21628  isbasis3g  21800  opnssneib  21966  ssidcn  22106  qtopcld  22564  mdegleb  24916  vieta1  25159  lgsne0  26170  axpasch  26986  0wlk  28153  0clwlk  28167  shlesb1i  29421  chnlei  29520  pjneli  29758  cvexchlem  30403  dmdbr5ati  30457  elimifd  30559  lmxrge0  31570  cntnevol  31862  bnj110  32505  goeleq12bg  32978  fmlafvel  33014  elpotr  33427  naddid1  33522  dfbigcup2  33887  bj-rexvw  34752  bj-rababw  34753  bj-brab2a1  35004  finxpreclem4  35251  wl-cases2-dnf  35357  wl-euae  35362  wl-dfclab  35433  cnambfre  35511  triantru3  36066  lub0N  36889  glb0N  36893  cvlsupr3  37044  isdomn3  40673  ifpdfor2  40694  ifpdfor  40698  ifpim1  40702  ifpid2  40704  ifpim2  40705  ifpid2g  40726  ifpid1g  40727  ifpim23g  40728  ifpim1g  40734  ifpimimb  40737  rp-isfinite6  40751  rababg  40798  relnonrel  40812  dffrege115  41204  funressnfv  44152  dfnelbr2  44380