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  949  truan  1415  rexv  2832  reuv  2833  rmov  2834  rabab  2835  euxfrdc  3003  euind  3004  dfdif3  3329  ddifstab  3351  vss  3556  mptv  4207  regexmidlem1  4655  peano5  4720  intirr  5149  fvopab6  5774  riotav  6009  mpov  6143  opabn1stprc  6389  brtpos0  6483  frec0g  6628  inl11  7356  apreim  8877  ccatlcan  11410  clim0  11970  gcd0id  12675  nnwosdc  12735  gsum0g  13609  isbasis3g  14911  opnssneib  15021  ssidcn  15075  bj-d0clsepcl  16695