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  949  truan  1415  rexv  2822  reuv  2823  rmov  2824  rabab  2825  euxfrdc  2993  euind  2994  dfdif3  3319  ddifstab  3341  vss  3544  mptv  4191  regexmidlem1  4637  peano5  4702  intirr  5130  fvopab6  5752  riotav  5987  mpov  6121  opabn1stprc  6367  brtpos0  6461  frec0g  6606  inl11  7307  apreim  8825  ccatlcan  11348  clim0  11908  gcd0id  12613  nnwosdc  12673  gsum0g  13542  isbasis3g  14840  opnssneib  14950  ssidcn  15004  bj-d0clsepcl  16624