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  909  cases  962  truan  1386  2sb5rf  2159  rexv  2985  reuv  2986  rmov  2987  rabab  2988  euxfr  3143  euind  3144  ddif  3486  nssinpss  3580  nsspssun  3581  vss  3713  difsnpss  4014  sspr  4034  sstp  4035  disjprg  4286  mptv  4382  reusv2lem5  4495  reusv7OLD  4502  oteqex2  4581  intirr  5214  xpcan  5272  fvopab6  5794  fnressn  5892  fnsuppresOLD  5936  riotav  6055  mpt2v  6178  sorpss  6363  fparlem2  6671  fnsuppres  6714  brtpos0  6750  genpass  9176  nnwos  10920  hashbclem  12203  wrdeqswrdlsw  12341  ccatlcan  12364  clim0  12982  gcd0id  13705  pjfval2  18132  isbasis3g  18552  opnssneib  18717  ssidcn  18857  qtopcld  19284  mdegleb  21533  vieta1  21776  lgsne0  22670  axpasch  23185  0wlk  23442  0trl  23443  shlesb1i  24787  chnlei  24886  pjneli  25124  cvexchlem  25770  dmdbr5ati  25824  elimifd  25903  elim2if  25904  lmxrge0  26380  cntnevol  26640  dfid4  27380  elpotr  27592  nofulllem1  27841  dfbigcup2  27928  cnambfre  28437  isdomn3  29569  mat1dimbas  30865  pmatcollpw2lem  30902  bnj110  31848  bj-rexvwv  32374  bj-rababwv  32375  lub0N  32831  glb0N  32835  cvlsupr3  32986