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  942  truan  1381  rexv  2781  reuv  2782  rmov  2783  rabab  2784  euxfrdc  2950  euind  2951  dfdif3  3273  ddifstab  3295  vss  3498  mptv  4130  regexmidlem1  4569  peano5  4634  intirr  5056  fvopab6  5658  riotav  5883  mpov  6012  brtpos0  6310  frec0g  6455  inl11  7131  apreim  8630  clim0  11450  gcd0id  12146  nnwosdc  12206  gsum0g  13039  isbasis3g  14282  opnssneib  14392  ssidcn  14446  bj-d0clsepcl  15571