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