Theorem biantrur 506

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)

Hypothesis

Ref	Expression
biantrur.1

Assertion

Ref	Expression
biantrur

Proof of Theorem biantrur

Step	Hyp	Ref	Expression
1		biantrur.1	. 2
2		ibar 504	. 2
3	1, 2	ax-mp 5	1

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

This theorem is referenced by:  mpbiran  918  cases  970  truan  1412  2sb5rf  2195  rexv  3124  reuv  3125  rmov  3126  rabab  3127  euxfr  3285  euind  3286  ddif  3635  nssinpss  3729  nsspssun  3730  vss  3863  difsnpss  4173  sspr  4193  sstp  4194  disjprg  4448  mptv  4544  reusv2lem5  4657  reusv7OLD  4664  oteqex2  4744  intirr  5390  xpcan  5448  fvopab6  5980  fnressn  6083  fnsuppresOLD  6131  riotav  6262  mpt2v  6392  sorpss  6585  fparlem2  6901  fnsuppres  6946  brtpos0  6981  genpass  9408  nnwos  11178  hashbclem  12501  wrdeqswrdlsw  12674  ccatlcan  12697  clim0  13329  gcd0id  14161  pjfval2  18740  mat1dimbas  18974  pmatcollpw2lem  19278  isbasis3g  19450  opnssneib  19616  ssidcn  19756  qtopcld  20214  mdegleb  22464  vieta1  22708  lgsne0  23608  axpasch  24244  0wlk  24547  0trl  24548  shlesb1i  26304  chnlei  26403  pjneli  26641  cvexchlem  27287  dmdbr5ati  27341  elimifd  27421  lmxrge0  27934  cntnevol  28199  dfid4  29103  elpotr  29213  nofulllem1  29462  dfbigcup2  29549  cnambfre  30063  isdomn3  31164  bnj110  33916  bj-rexvwv  34442  bj-rababwv  34443  lub0N  34914  glb0N  34918  cvlsupr3  35069  bj-ifid1g  37708  bj-ifid2g  37709  bj-ifid2  37711  bj-ifim1  37712  bj-ifim2  37713  bj-ifim1g  37714  bj-ifimimb  37715  bj-ifdfor  37722  bj-ifdfor2  37723  rp-isfinite6  37744  rp-imass  37795

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