Theorem biantrur 506

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

Syntax hints:   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  mpbiran  918  cases  970  truan  1400  2sb5rf  2181  rexv  3110  reuv  3111  rmov  3112  rabab  3113  euxfr  3271  euind  3272  ddif  3621  nssinpss  3715  nsspssun  3716  vss  3849  difsnpss  4158  sspr  4178  sstp  4179  disjprg  4433  mptv  4529  reusv2lem5  4642  reusv7OLD  4649  oteqex2  4729  intirr  5375  xpcan  5433  fvopab6  5965  fnressn  6068  fnsuppresOLD  6116  riotav  6247  mpt2v  6377  sorpss  6570  fparlem2  6886  fnsuppres  6929  brtpos0  6964  genpass  9390  nnwos  11159  hashbclem  12482  wrdeqswrdlsw  12655  ccatlcan  12678  clim0  13310  gcd0id  14142  pjfval2  18717  mat1dimbas  18951  pmatcollpw2lem  19255  isbasis3g  19427  opnssneib  19593  ssidcn  19733  qtopcld  20191  mdegleb  22441  vieta1  22684  lgsne0  23584  axpasch  24220  0wlk  24523  0trl  24524  shlesb1i  26280  chnlei  26379  pjneli  26617  cvexchlem  27263  dmdbr5ati  27317  elimifd  27397  lmxrge0  27911  cntnevol  28176  dfid4  29080  elpotr  29188  nofulllem1  29437  dfbigcup2  29524  cnambfre  30038  isdomn3  31140  bnj110  33649  bj-rexvwv  34190  bj-rababwv  34191  lub0N  34654  glb0N  34658  cvlsupr3  34809  rp-isfinite6  37447  rp-imass  37482