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 513  pm5.32 642  hban 1006  19.29 1067  19.35 1071  equsex 1148  sban 1232  r19.35 1751  aceq5lem4 4710  kmlem3 4739  nmcopexlem1 9866  nmcfnexlem1 9895

Copyright terms: Public domain