Theorem biantrur 303

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

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  942  truan  1381  rexv  2778  reuv  2779  rmov  2780  rabab  2781  euxfrdc  2946  euind  2947  dfdif3  3269  ddifstab  3291  vss  3494  mptv  4126  regexmidlem1  4565  peano5  4630  intirr  5052  fvopab6  5654  riotav  5879  mpov  6008  brtpos0  6305  frec0g  6450  inl11  7124  apreim  8622  clim0  11428  gcd0id  12116  nnwosdc  12176  gsum0g  12979  isbasis3g  14214  opnssneib  14324  ssidcn  14378  bj-d0clsepcl  15417