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  11538  gcd0id  12242  nnwosdc  12302  gsum0g  13170  isbasis3g  14460  opnssneib  14570  ssidcn  14624  bj-d0clsepcl  15794