Theorem biantrur 301

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 299	. 2 |- ( ph -> ( ps <-> ( ph /\ ps ) ) )
3	1, 2	ax-mp 5	1 |- ( ps <-> ( ph /\ ps ) )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbiran  924  truan  1348  rexv  2704  reuv  2705  rmov  2706  rabab  2707  euxfrdc  2870  euind  2871  dfdif3  3186  ddifstab  3208  vss  3410  mptv  4025  regexmidlem1  4448  peano5  4512  intirr  4925  fvopab6  5517  riotav  5735  mpov  5861  brtpos0  6149  frec0g  6294  inl11  6950  apreim  8365  clim0  11054  gcd0id  11667  isbasis3g  12213  opnssneib  12325  ssidcn  12379  bj-d0clsepcl  13123