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  924  truan  1348  rexv  2699  reuv  2700  rmov  2701  rabab  2702  euxfrdc  2865  euind  2866  dfdif3  3181  ddifstab  3203  vss  3405  mptv  4020  regexmidlem1  4443  peano5  4507  intirr  4920  fvopab6  5510  riotav  5728  mpov  5854  brtpos0  6142  frec0g  6287  inl11  6943  apreim  8358  clim0  11047  gcd0id  11656  isbasis3g  12202  opnssneib  12314  ssidcn  12368  bj-d0clsepcl  13112