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  3274  ddifstab  3296  vss  3499  mptv  4131  regexmidlem1  4570  peano5  4635  intirr  5057  fvopab6  5661  riotav  5886  mpov  6016  brtpos0  6319  frec0g  6464  inl11  7140  apreim  8649  clim0  11469  gcd0id  12173  nnwosdc  12233  gsum0g  13100  isbasis3g  14390  opnssneib  14500  ssidcn  14554  bj-d0clsepcl  15679