New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  biantrur GIF 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 8 1 (ψ ↔ (φ ψ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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