Theorem biantrur 509

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

Syntax hints:   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  mpbiran  929  cases  982  truan  1461  2sb5rf  2280  rexv  3062  reuv  3063  rmov  3064  rabab  3065  euxfr  3224  euind  3225  ddif  3565  nssinpss  3675  nsspssun  3676  vss  3801  difsnpss  4115  sspr  4135  sstp  4136  disjprg  4398  mptv  4496  reusv2lem5  4608  oteqex2  4693  dfid4  4751  intirr  5218  xpcan  5273  fvopab6  5975  fnressn  6076  riotav  6257  mpt2v  6386  sorpss  6576  fparlem2  6897  fnsuppres  6942  brtpos0  6980  sup0riota  7979  genpass  9434  nnwos  11226  hashbclem  12615  ccatlcan  12828  clim0  13570  gcd0id  14487  pjfval2  19272  mat1dimbas  19497  pmatcollpw2lem  19801  isbasis3g  19964  opnssneib  20131  ssidcn  20271  qtopcld  20728  mdegleb  23013  vieta1  23265  lgsne0  24261  axpasch  24971  0wlk  25275  0trl  25276  shlesb1i  27039  chnlei  27138  pjneli  27376  cvexchlem  28021  dmdbr5ati  28075  elimifd  28160  lmxrge0  28758  cntnevol  29050  bnj110  29669  elpotr  30427  nofulllem1  30591  dfbigcup2  30666  bj-rexvwv  31475  bj-rababwv  31476  finxpreclem4  31786  wl-cases2-dnf  31850  cnambfre  31989  lub0N  32755  glb0N  32759  cvlsupr3  32910  isdomn3  36081  ifpdfor2  36104  ifpdfor  36108  ifpim1  36112  ifpid2  36114  ifpim2  36115  ifpid2g  36137  ifpid1g  36138  ifpim23g  36139  ifpim1g  36145  ifpimimb  36148  rp-isfinite6  36163  rababg  36179  relnonrel  36193  rp-imass  36366  dffrege115  36574  opabn1stprc  39007  01wlk  39704