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  946  truan  1412  rexv  2819  reuv  2820  rmov  2821  rabab  2822  euxfrdc  2990  euind  2991  dfdif3  3315  ddifstab  3337  vss  3540  mptv  4184  regexmidlem1  4629  peano5  4694  intirr  5121  fvopab6  5739  riotav  5972  mpov  6106  opabn1stprc  6353  brtpos0  6413  frec0g  6558  inl11  7255  apreim  8773  ccatlcan  11289  clim0  11836  gcd0id  12540  nnwosdc  12600  gsum0g  13469  isbasis3g  14760  opnssneib  14870  ssidcn  14924  bj-d0clsepcl  16456