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  940  truan  1370  rexv  2755  reuv  2756  rmov  2757  rabab  2758  euxfrdc  2923  euind  2924  dfdif3  3245  ddifstab  3267  vss  3470  mptv  4100  regexmidlem1  4532  peano5  4597  intirr  5015  fvopab6  5612  riotav  5835  mpov  5964  brtpos0  6252  frec0g  6397  inl11  7063  apreim  8558  clim0  11288  gcd0id  11974  nnwosdc  12034  isbasis3g  13437  opnssneib  13549  ssidcn  13603  bj-d0clsepcl  14559