Theorem biantrur 301

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 299	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiran  925  truan  1349  rexv  2707  reuv  2708  rmov  2709  rabab  2710  euxfrdc  2874  euind  2875  dfdif3  3191  ddifstab  3213  vss  3415  mptv  4033  regexmidlem1  4456  peano5  4520  intirr  4933  fvopab6  5525  riotav  5743  mpov  5869  brtpos0  6157  frec0g  6302  inl11  6958  apreim  8389  clim0  11086  gcd0id  11703  isbasis3g  12252  opnssneib  12364  ssidcn  12418  bj-d0clsepcl  13294