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  2792  reuv  2793  rmov  2794  rabab  2795  euxfrdc  2963  euind  2964  dfdif3  3287  ddifstab  3309  vss  3512  mptv  4152  regexmidlem1  4594  peano5  4659  intirr  5083  fvopab6  5694  riotav  5923  mpov  6053  brtpos0  6356  frec0g  6501  inl11  7188  apreim  8706  ccatlcan  11204  clim0  11681  gcd0id  12385  nnwosdc  12445  gsum0g  13313  isbasis3g  14603  opnssneib  14713  ssidcn  14767  bj-d0clsepcl  16030