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  930  truan  1360  rexv  2744  reuv  2745  rmov  2746  rabab  2747  euxfrdc  2912  euind  2913  dfdif3  3232  ddifstab  3254  vss  3456  mptv  4079  regexmidlem1  4510  peano5  4575  intirr  4990  fvopab6  5582  riotav  5803  mpov  5932  brtpos0  6220  frec0g  6365  inl11  7030  apreim  8501  clim0  11226  gcd0id  11912  nnwosdc  11972  isbasis3g  12684  opnssneib  12796  ssidcn  12850  bj-d0clsepcl  13807