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  1389  rexv  2789  reuv  2790  rmov  2791  rabab  2792  euxfrdc  2958  euind  2959  dfdif3  3282  ddifstab  3304  vss  3507  mptv  4140  regexmidlem1  4580  peano5  4645  intirr  5068  fvopab6  5675  riotav  5904  mpov  6034  brtpos0  6337  frec0g  6482  inl11  7166  apreim  8675  clim0  11567  gcd0id  12271  nnwosdc  12331  gsum0g  13199  isbasis3g  14489  opnssneib  14599  ssidcn  14653  bj-d0clsepcl  15823