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  3006  euind  3007  dfdif3  3333  ddifstab  3355  vss  3560  mptv  4212  regexmidlem1  4660  peano5  4725  intirr  5154  fvopab6  5779  riotav  6017  mpov  6151  opabn1stprc  6402  brtpos0  6496  frec0g  6641  inl11  7369  apreim  8895  ccatlcan  11438  clim0  11998  gcd0id  12703  nnwosdc  12763  gsum0g  13662  isbasis3g  15040  opnssneib  15150  ssidcn  15204  bj-d0clsepcl  16834