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

Theorem biantru 491
 Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biantru.1 φ
Assertion
Ref Expression
biantru (ψ ↔ (ψ φ))

Proof of Theorem biantru
StepHypRef Expression
1 biantru.1 . 2 φ
2 iba 489 . 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:  pm4.71  611  mpbiran2  885  isset  2863  rexcom4b  2880  eueq  3008  nsspssun  3488  disjpss  3601  elvvk  4207  eqtfinrelk  4486  phiall  4618  dfid3  4768  resopab  4999  xpcan2  5058  funfn  5136  dffn2  5224  dffn3  5229  dffn4  5275  f1orn  5296  fsn  5432  ce0nnul  6177  ce0nulnc  6184  dmsnfn  6327
 Copyright terms: Public domain W3C validator