Theorem biantrur 527

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

Syntax hints:   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  mpbiran  953  cases  992  truan  1501  2sb5rf  2451  rexv  3220  reuv  3221  rmov  3222  rabab  3223  euxfr  3392  euind  3393  ddif  3742  nssinpss  3856  nsspssun  3857  vss  4012  difsnpss  4338  sspr  4366  sstp  4367  disjprg  4648  mptv  4751  reusv2lem5  4873  oteqex2  4963  dfid4  5026  intirr  5514  xpcan  5570  fvopab6  6310  fnressn  6425  riotav  6616  mpt2v  6750  sorpss  6942  opabn1stprc  7228  fparlem2  7278  fnsuppres  7322  brtpos0  7359  sup0riota  8371  genpass  9831  nnwos  11755  hashbclem  13236  ccatlcan  13472  clim0  14237  gcd0id  15240  pjfval2  20053  mat1dimbas  20278  pmatcollpw2lem  20582  isbasis3g  20753  opnssneib  20919  ssidcn  21059  qtopcld  21516  mdegleb  23824  vieta1  24067  lgsne0  25060  axpasch  25821  0wlk  26977  0clwlk  26991  shlesb1i  28245  chnlei  28344  pjneli  28582  cvexchlem  29227  dmdbr5ati  29281  elimifd  29362  lmxrge0  29998  cntnevol  30291  bnj110  30928  elpotr  31686  dfbigcup2  32006  bj-cleljustab  32847  bj-rexvwv  32866  bj-rababwv  32867  finxpreclem4  33231  wl-cases2-dnf  33295  cnambfre  33458  triantru3  34000  lub0N  34476  glb0N  34480  cvlsupr3  34631  isdomn3  37782  ifpdfor2  37805  ifpdfor  37809  ifpim1  37813  ifpid2  37815  ifpim2  37816  ifpid2g  37838  ifpid1g  37839  ifpim23g  37840  ifpim1g  37846  ifpimimb  37849  rp-isfinite6  37864  rababg  37879  relnonrel  37893  rp-imass  38065  dffrege115  38272  dfnelbr2  41290