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  948  truan  1414  rexv  2820  reuv  2821  rmov  2822  rabab  2823  euxfrdc  2991  euind  2992  dfdif3  3316  ddifstab  3338  vss  3541  mptv  4187  regexmidlem1  4633  peano5  4698  intirr  5125  fvopab6  5746  riotav  5982  mpov  6116  opabn1stprc  6363  brtpos0  6423  frec0g  6568  inl11  7269  apreim  8788  ccatlcan  11308  clim0  11868  gcd0id  12573  nnwosdc  12633  gsum0g  13502  isbasis3g  14799  opnssneib  14909  ssidcn  14963  bj-d0clsepcl  16580