Theorem biantrur 297

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)

Hypothesis

Ref	Expression
biantrur.1	|- ph

Assertion

Ref	Expression
biantrur	|- ( ps <-> ( ph /\ ps ) )

Proof of Theorem biantrur

Step	Hyp	Ref	Expression
1		biantrur.1	. 2 |- ph
2		ibar 295	. 2 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )
3	1, 2	ax-mp 7	1 |- ( ps <-> ( ph /\ ps ) )

Syntax hints:   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpbiran  881  truan  1301  rexv  2617  reuv  2618  rmov  2619  rabab  2620  euxfrdc  2778  euind  2779  ddifstab  3104  vss  3291  mptv  3874  regexmidlem1  4276  peano5  4339  intirr  4731  fvopab6  5285  riotav  5493  mpt2v  5614  brtpos0  5890  frec0g  6006  apreim  7703  clim0  10124  gcd0id  10370  bj-d0clsepcl  10720