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  949  truan  1415  rexv  2834  reuv  2835  rmov  2836  rabab  2837  euxfrdc  3005  euind  3006  dfdif3  3331  ddifstab  3353  vss  3558  mptv  4209  regexmidlem1  4657  peano5  4722  intirr  5151  fvopab6  5776  riotav  6011  mpov  6145  opabn1stprc  6391  brtpos0  6485  frec0g  6630  inl11  7358  apreim  8882  ccatlcan  11418  clim0  11978  gcd0id  12683  nnwosdc  12743  gsum0g  13630  isbasis3g  14960  opnssneib  15070  ssidcn  15124  bj-d0clsepcl  16744