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  946  truan  1412  rexv  2818  reuv  2819  rmov  2820  rabab  2821  euxfrdc  2989  euind  2990  dfdif3  3314  ddifstab  3336  vss  3539  mptv  4181  regexmidlem1  4626  peano5  4691  intirr  5118  fvopab6  5736  riotav  5969  mpov  6103  opabn1stprc  6350  brtpos0  6409  frec0g  6554  inl11  7248  apreim  8766  ccatlcan  11271  clim0  11817  gcd0id  12521  nnwosdc  12581  gsum0g  13450  isbasis3g  14741  opnssneib  14851  ssidcn  14905  bj-d0clsepcl  16397