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  943  truan  1390  rexv  2790  reuv  2791  rmov  2792  rabab  2793  euxfrdc  2959  euind  2960  dfdif3  3283  ddifstab  3305  vss  3508  mptv  4141  regexmidlem1  4581  peano5  4646  intirr  5069  fvopab6  5676  riotav  5905  mpov  6035  brtpos0  6338  frec0g  6483  inl11  7167  apreim  8676  clim0  11596  gcd0id  12300  nnwosdc  12360  gsum0g  13228  isbasis3g  14518  opnssneib  14628  ssidcn  14682  bj-d0clsepcl  15861