NFE Home 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 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:  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