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  935  truan  1365  rexv  2748  reuv  2749  rmov  2750  rabab  2751  euxfrdc  2916  euind  2917  dfdif3  3237  ddifstab  3259  vss  3462  mptv  4086  regexmidlem1  4517  peano5  4582  intirr  4997  fvopab6  5592  riotav  5814  mpov  5943  brtpos0  6231  frec0g  6376  inl11  7042  apreim  8522  clim0  11248  gcd0id  11934  nnwosdc  11994  isbasis3g  12838  opnssneib  12950  ssidcn  13004  bj-d0clsepcl  13960