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

Definition df-an 360
Description: Define conjunction (logical 'and'). Definition of [Margaris] p. 49. When both the left and right operand are true, the result is true; when either is false, the result is false. For example, it is true that (2 = 2 3 = 3). After we define the constant true (df-tru 1319) and the constant false (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ⊤ ) ↔ ⊤ ) (truantru 1336), (( ⊤ ⊥ ) ↔ ⊥ ) (truanfal 1337), (( ⊥ ⊤ ) ↔ ⊥ ) (falantru 1338), and (( ⊥ ⊥ ) ↔ ⊥ ) (falanfal 1339).

Contrast with (df-or 359), (wi 4), (df-nan 1288), and (df-xor 1305) . (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
df-an ((φ ψ) ↔ ¬ (φ → ¬ ψ))

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 wph . . 3 wff φ
2 wps . . 3 wff ψ
31, 2wa 358 . 2 wff (φ ψ)
42wn 3 . . . 4 wff ¬ ψ
51, 4wi 4 . . 3 wff (φ → ¬ ψ)
65wn 3 . 2 wff ¬ (φ → ¬ ψ)
73, 6wb 176 1 wff ((φ ψ) ↔ ¬ (φ → ¬ ψ))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.63  410  imnan  411  imp  418  ex  423  pm4.54  479  dfbi2  609  pm5.32  617  nfand  1822  nfanOLD  1826  hbanOLD  1829  equsex  1962  sban  2069  r19.35  2758  disj  3591
  Copyright terms: Public domain W3C validator