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  2821  reuv  2822  rmov  2823  rabab  2824  euxfrdc  2992  euind  2993  dfdif3  3317  ddifstab  3339  vss  3542  mptv  4186  regexmidlem1  4631  peano5  4696  intirr  5123  fvopab6  5743  riotav  5977  mpov  6111  opabn1stprc  6358  brtpos0  6418  frec0g  6563  inl11  7264  apreim  8783  ccatlcan  11300  clim0  11847  gcd0id  12552  nnwosdc  12612  gsum0g  13481  isbasis3g  14773  opnssneib  14883  ssidcn  14937  bj-d0clsepcl  16541