Theorem biantrur 303

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	. 2 ⊢ 𝜑
2		ibar 301	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiran  949  truan  1415  rexv  2834  reuv  2835  rmov  2836  rabab  2837  euxfrdc  3006  euind  3007  dfdif3  3333  ddifstab  3355  vss  3560  mptv  4212  regexmidlem1  4660  peano5  4725  intirr  5154  fvopab6  5779  riotav  6017  mpov  6151  opabn1stprc  6402  brtpos0  6496  frec0g  6641  inl11  7369  apreim  8894  ccatlcan  11435  clim0  11995  gcd0id  12700  nnwosdc  12760  gsum0g  13659  isbasis3g  15037  opnssneib  15147  ssidcn  15201  bj-d0clsepcl  16821