Theorem biantrur 504

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

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

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 369

This theorem is referenced by:  mpbiran  916  cases  968  truan  1415  2sb5rf  2197  rexv  3121  reuv  3122  rmov  3123  rabab  3124  euxfr  3282  euind  3283  ddif  3622  nssinpss  3727  nsspssun  3728  vss  3851  difsnpss  4159  sspr  4179  sstp  4180  disjprg  4435  mptv  4531  reusv2lem5  4642  reusv7OLD  4649  oteqex2  4728  intirr  5373  xpcan  5428  fvopab6  5956  fnressn  6059  fnsuppresOLD  6107  riotav  6237  mpt2v  6365  sorpss  6558  fparlem2  6874  fnsuppres  6919  brtpos0  6954  genpass  9376  nnwos  11150  hashbclem  12488  ccatlcan  12691  clim0  13414  gcd0id  14248  pjfval2  18916  mat1dimbas  19144  pmatcollpw2lem  19448  isbasis3g  19620  opnssneib  19786  ssidcn  19926  qtopcld  20383  mdegleb  22633  vieta1  22877  lgsne0  23809  axpasch  24449  0wlk  24752  0trl  24753  shlesb1i  26505  chnlei  26604  pjneli  26842  cvexchlem  27488  dmdbr5ati  27542  elimifd  27630  lmxrge0  28172  cntnevol  28439  dfid4  29347  elpotr  29456  nofulllem1  29705  dfbigcup2  29780  wl-cases2-dnf  30213  cnambfre  30306  isdomn3  31408  bnj110  34336  bj-rexvwv  34862  bj-rababwv  34863  lub0N  35330  glb0N  35334  cvlsupr3  35485  ifpid1g  38125  ifpid2g  38126  ifpid2  38128  ifpim1  38129  ifpim2  38130  ifpim23g  38131  ifpim1g  38134  ifpimimb  38135  ifpdfor  38147  ifpdfor2  38148  rp-isfinite6  38176  rp-imass  38268  dffrege115  38479