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  2947  euind  2948  dfdif3  3270  ddifstab  3292  vss  3495  mptv  4127  regexmidlem1  4566  peano5  4631  intirr  5053  fvopab6  5655  riotav  5880  mpov  6009  brtpos0  6307  frec0g  6452  inl11  7126  apreim  8624  clim0  11431  gcd0id  12119  nnwosdc  12179  gsum0g  12982  isbasis3g  14225  opnssneib  14335  ssidcn  14389  bj-d0clsepcl  15487