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  2831  reuv  2832  rmov  2833  rabab  2834  euxfrdc  3002  euind  3003  dfdif3  3328  ddifstab  3350  vss  3555  mptv  4206  regexmidlem1  4654  peano5  4719  intirr  5148  fvopab6  5773  riotav  6008  mpov  6142  opabn1stprc  6388  brtpos0  6482  frec0g  6627  inl11  7355  apreim  8873  ccatlcan  11403  clim0  11963  gcd0id  12668  nnwosdc  12728  gsum0g  13598  isbasis3g  14898  opnssneib  15008  ssidcn  15062  bj-d0clsepcl  16682