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  943  truan  1390  rexv  2790  reuv  2791  rmov  2792  rabab  2793  euxfrdc  2959  euind  2960  dfdif3  3283  ddifstab  3305  vss  3508  mptv  4142  regexmidlem1  4582  peano5  4647  intirr  5070  fvopab6  5678  riotav  5907  mpov  6037  brtpos0  6340  frec0g  6485  inl11  7169  apreim  8678  clim0  11629  gcd0id  12333  nnwosdc  12393  gsum0g  13261  isbasis3g  14551  opnssneib  14661  ssidcn  14715  bj-d0clsepcl  15898