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  953  truan  1419  rexv  2840  reuv  2841  rmov  2842  rabab  2843  euxfrdc  3012  euind  3013  dfdif3  3339  ddifstab  3361  vss  3567  mptv  4223  regexmidlem1  4675  peano5  4740  intirr  5169  fvopab6  5796  riotav  6034  mpov  6168  opabn1stprc  6419  brtpos0  6513  frec0g  6658  inl11  7395  apreim  8921  ccatlcan  11468  clim0  12029  gcd0id  12734  nnwosdc  12794  gzsum0  13690  isbasis3g  15070  opnssneib  15180  ssidcn  15234  bj-d0clsepcl  16865