Definition df-an 198

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 196	. 2 wff (φ ∧ ψ)
4	2	wn 1	. . . 4 wff ¬ ψ
5	1, 4	wi 2	. . 3 wff (φ → ¬ ψ)
6	5	wn 1	. 2 wff ¬ (φ → ¬ ψ)
7	3, 6	wb 127	1 wff ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ))

This definition is referenced by:  iman 205  imnan 207  pm3.2 232  jca 236  anor 252  pm3.26 256  pm3.27 260  impexp 276  imp 277  exp 291  anass 336  bi 396  pm5.32 488  hban 704  19.29 752  19.35 754  eqsex 834  sban 889  r19.35 1298  aceq5lem4 3561  kmlem3 3582

metamath.org