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 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbiran  953  truan  1419  rexv  2840  reuv  2841  rmov  2842  rabab  2843  euxfrdc  3012  euind  3013  dfdif3  3339  ddifstab  3361  vss  3568  mptv  4228  regexmidlem1  4680  peano5  4745  intirr  5174  fvopab6  5805  riotav  6044  mpov  6178  opabn1stprc  6429  brtpos0  6523  frec0g  6668  inl11  7405  apreim  8933  ccatlcan  11504  clim0  12067  gcd0id  12772  nnwosdc  12832  gzsum0  13762  isbasis3g  15196  opnssneib  15306  ssidcn  15360  bj-d0clsepcl  17049