Theorem biantrur 508

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

Syntax hints:   <-> wb 187   /\ wa 370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188  df-an 372

This theorem is referenced by:  mpbiran  926  cases  979  truan  1454  2sb5rf  2246  rexv  3096  reuv  3097  rmov  3098  rabab  3099  euxfr  3257  euind  3258  ddif  3597  nssinpss  3705  nsspssun  3706  vss  3829  difsnpss  4140  sspr  4160  sstp  4161  disjprg  4416  mptv  4514  reusv2lem5  4626  oteqex2  4709  dfid4  4767  intirr  5234  xpcan  5289  fvopab6  5987  fnressn  6088  riotav  6269  mpt2v  6397  sorpss  6587  fparlem2  6905  fnsuppres  6950  brtpos0  6985  sup0riota  7982  genpass  9435  nnwos  11227  hashbclem  12613  ccatlcan  12819  clim0  13558  gcd0id  14475  pjfval2  19259  mat1dimbas  19484  pmatcollpw2lem  19788  isbasis3g  19951  opnssneib  20118  ssidcn  20258  qtopcld  20715  mdegleb  23000  vieta1  23252  lgsne0  24248  axpasch  24958  0wlk  25261  0trl  25262  shlesb1i  27025  chnlei  27124  pjneli  27362  cvexchlem  28007  dmdbr5ati  28061  elimifd  28150  lmxrge0  28754  cntnevol  29046  bnj110  29665  elpotr  30422  nofulllem1  30584  dfbigcup2  30659  bj-rexvwv  31433  bj-rababwv  31434  wl-cases2-dnf  31764  cnambfre  31903  lub0N  32674  glb0N  32678  cvlsupr3  32829  isdomn3  36001  ifpdfor2  36024  ifpdfor  36028  ifpim1  36032  ifpid2  36034  ifpim2  36035  ifpid2g  36057  ifpid1g  36058  ifpim23g  36059  ifpim1g  36065  ifpimimb  36068  rp-isfinite6  36083  rp-imass  36224  dffrege115  36432