Definition df-an

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 T. ( df-tru ) and the constant false F. ( df-fal ), we will be able to prove these truth table values: ( ( T. /\ T. ) <-> T. ) ( truantru ), ( ( T. /\ F. ) <-> F. ) ( truanfal ), ( ( F. /\ T. ) <-> F. ) ( falantru ), and ( ( F. /\ F. ) <-> F. ) ( falanfal ).

This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute -. ( ph -> -. ps ) for ( ph /\ ps ) , we end up with an instance of previously proved theorem biid . This is the justification for the definition, along with the fact that it introduces a new symbol /\ . Contrast with \/ ( df-or ), -> ( wi ), -/\ ( df-nan ), and \/_ ( df-xor ). (Contributed by NM, 5-Jan-1993)

	Ref	Expression
Assertion	df-an	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ¬ ( 𝜑 → ¬ 𝜓 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2	0 1	wa	⊢ ( 𝜑 ∧ 𝜓 )
3	1	wn	⊢ ¬ 𝜓
4	0 3	wi	⊢ ( 𝜑 → ¬ 𝜓 )
5	4	wn	⊢ ¬ ( 𝜑 → ¬ 𝜓 )
6	2 5	wb	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ¬ ( 𝜑 → ¬ 𝜓 ) )