Definition df-an 225

Description: Define conjunction (logical 'and'). Definition of [Margaris] p. 49.

Assertion

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

Detailed syntax breakdown of Definition df-an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3	1, 2	wa 223	. 2 wff (φ ⋀ ψ)
4	2	wn 2	. . . 4 wff ¬ ψ
5	1, 4	wi 3	. . 3 wff (φ → ¬ ψ)
6	5	wn 2	. 2 wff ¬ (φ → ¬ ψ)
7	3, 6	wb 146	1 wff ((φ ⋀ ψ) ↔ ¬ (φ → ¬ ψ))

This definition is referenced by:  pm4.63 228  iman 237  imnan 242  pm3.2 283  jca 288  anor 304  pm3.26 319  pm3.27 323  impexp 347  anass 439  bi 514  pm5.32 643  hban 1008  19.29 1070  19.35 1074  equsex 1151  sban 1236  r19.35 1757  aceq5lem4 4721  kmlem3 4750  nmcopexlem1 9907  nmcfnexlem1 9936

Copyright terms: Public domain