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  911  cases  964  truan  1391  2sb5rf  2174  rexv  3121  reuv  3122  rmov  3123  rabab  3124  euxfr  3282  euind  3283  ddif  3629  nssinpss  3723  nsspssun  3724  vss  3856  difsnpss  4163  sspr  4183  sstp  4184  disjprg  4436  mptv  4532  reusv2lem5  4645  reusv7OLD  4652  oteqex2  4732  intirr  5376  xpcan  5434  fvopab6  5965  fnressn  6064  fnsuppresOLD  6112  riotav  6241  mpt2v  6367  sorpss  6560  fparlem2  6874  fnsuppres  6917  brtpos0  6952  genpass  9376  nnwos  11138  hashbclem  12454  wrdeqswrdlsw  12624  ccatlcan  12647  clim0  13278  gcd0id  14009  pjfval2  18500  mat1dimbas  18734  pmatcollpw2lem  19038  isbasis3g  19210  opnssneib  19375  ssidcn  19515  qtopcld  19942  mdegleb  22192  vieta1  22435  lgsne0  23329  axpasch  23913  0wlk  24209  0trl  24210  shlesb1i  25966  chnlei  26065  pjneli  26303  cvexchlem  26949  dmdbr5ati  27003  elimifd  27081  elim2if  27082  lmxrge0  27556  cntnevol  27825  dfid4  28564  elpotr  28776  nofulllem1  29025  dfbigcup2  29112  cnambfre  29627  isdomn3  30758  bnj110  32870  bj-rexvwv  33398  bj-rababwv  33399  lub0N  33861  glb0N  33865  cvlsupr3  34016  rp-imass  36671