Theorem biantrur 531

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  mpbiran  707  cases  1041  truan  1552  2sb5rf  2471  euae  2655  rexv  3499  reuv  3500  rmov  3501  rabab  3502  euxfrw  3717  euxfr  3719  euind  3720  dfdif3  4114  ddif  4136  nssinpss  4256  nsspssun  4257  notabw  4303  vss  4443  reuprg0  4706  reuprg  4707  difsnpss  4810  sspr  4836  sstp  4837  disjprgw  5143  disjprg  5144  mptv  5264  reusv2lem5  5400  oteqex2  5499  dfid4  5575  intirr  6119  xpcan  6175  resssxp  6269  fvopab6  7031  fnressn  7158  riotav  7372  mpov  7522  sorpss  7720  opabn1stprc  8046  fparlem2  8101  fnsuppres  8178  brtpos0  8220  naddrid  8684  sup0riota  9462  genpass  11006  nnwos  12903  hashbclem  14415  ccatlcan  14672  clim0  15454  gcd0id  16464  pjfval2  21483  mat1dimbas  22194  pmatcollpw2lem  22499  isbasis3g  22672  opnssneib  22839  ssidcn  22979  qtopcld  23437  mdegleb  25806  vieta1  26049  lgsne0  27062  axpasch  28454  0wlk  29624  0clwlk  29638  shlesb1i  30894  chnlei  30993  pjneli  31231  cvexchlem  31876  dmdbr5ati  31930  elimifd  32030  lmxrge0  33218  cntnevol  33512  bnj110  34155  goeleq12bg  34626  fmlafvel  34662  elpotr  35045  dfbigcup2  35163  bj-rexvw  36063  bj-rababw  36064  bj-brab2a1  36333  finxpreclem4  36578  wl-cases2-dnf  36684  wl-euae  36689  wl-dfclab  36761  cnambfre  36839  triantru3  37397  lub0N  38362  glb0N  38366  cvlsupr3  38517  isdomn3  42248  ifpdfor2  42514  ifpdfor  42518  ifpim1  42522  ifpid2  42524  ifpim2  42525  ifpid2g  42546  ifpid1g  42547  ifpim23g  42548  ifpim1g  42554  ifpimimb  42557  rp-isfinite6  42571  rababg  42627  relnonrel  42640  dffrege115  43031  funressnfv  46052  dfnelbr2  46280