Theorem biantrur 298

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 296	. 2 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )
3	1, 2	ax-mp 7	1 |- ( ps <-> ( ph /\ ps ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiran  887  truan  1307  rexv  2638  reuv  2639  rmov  2640  rabab  2641  euxfrdc  2802  euind  2803  dfdif3  3111  ddifstab  3133  vss  3334  mptv  3941  regexmidlem1  4362  peano5  4426  intirr  4831  fvopab6  5410  riotav  5627  mpt2v  5752  brtpos0  6031  frec0g  6176  apreim  8134  clim0  10727  gcd0id  11302  isbasis3g  11798  bj-d0clsepcl  12086