Theorem biantrur 301

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiran  925  truan  1352  rexv  2730  reuv  2731  rmov  2732  rabab  2733  euxfrdc  2898  euind  2899  dfdif3  3217  ddifstab  3239  vss  3441  mptv  4061  regexmidlem1  4490  peano5  4555  intirr  4969  fvopab6  5561  riotav  5779  mpov  5905  brtpos0  6193  frec0g  6338  inl11  6999  apreim  8461  clim0  11164  gcd0id  11843  isbasis3g  12404  opnssneib  12516  ssidcn  12570  bj-d0clsepcl  13459