NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  biantrur Unicode version

Theorem biantrur 492
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
StepHypRef Expression
1 biantrur.1 . 2
2 ibar 490 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:   wb 176   wa 358
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 177  df-an 360
This theorem is referenced by:  mpbiran  884  rexv  2873  reuv  2874  rmov  2875  rabab  2876  euxfr  3022  euind  3023  ddif  3398  nssinpss  3487  nsspssun  3488  vss  3587  elimif  3691  difsnpss  3851  sspr  3869  sstp  3870  elp6  4263  xpkvexg  4285  dfuni12  4291  addcid1  4405  vfinspsslem1  4550  xpcan  5057  ssrnres  5059  fvopabg  5391  fnressn  5438  rnoprab  5576  mptv  5718  mpt2v  5719  dmtxp  5802  pw1fnf1o  5855
  Copyright terms: Public domain W3C validator