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  2795  reuv  2796  rmov  2797  rabab  2798  euxfrdc  2966  euind  2967  dfdif3  3291  ddifstab  3313  vss  3516  mptv  4157  regexmidlem1  4599  peano5  4664  intirr  5088  fvopab6  5699  riotav  5928  mpov  6058  brtpos0  6361  frec0g  6506  inl11  7193  apreim  8711  ccatlcan  11209  clim0  11711  gcd0id  12415  nnwosdc  12475  gsum0g  13343  isbasis3g  14633  opnssneib  14743  ssidcn  14797  bj-d0clsepcl  16060