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  948  truan  1414  rexv  2821  reuv  2822  rmov  2823  rabab  2824  euxfrdc  2992  euind  2993  dfdif3  3317  ddifstab  3339  vss  3542  mptv  4186  regexmidlem1  4631  peano5  4696  intirr  5123  fvopab6  5743  riotav  5977  mpov  6111  opabn1stprc  6358  brtpos0  6418  frec0g  6563  inl11  7264  apreim  8783  ccatlcan  11303  clim0  11850  gcd0id  12555  nnwosdc  12615  gsum0g  13484  isbasis3g  14776  opnssneib  14886  ssidcn  14940  bj-d0clsepcl  16546