Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-an | Structured version Visualization version GIF version |
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 1478) and the constant false ⊥ (df-fal 1481), we will be able
to prove these truth table values: ((⊤ ∧
⊤) ↔ ⊤)
(truantru 1497), ((⊤ ∧ ⊥)
↔ ⊥) (truanfal 1498),
((⊥ ∧ ⊤) ↔ ⊥) (falantru 1499), and
((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1500).
Contrast with ∨ (df-or 384), → (wi 4), ⊼ (df-nan 1440), and ⊻ (df-xor 1457) . (Contributed by NM, 5-Jan-1993.) |
Ref | Expression |
---|---|
df-an | ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 1, 2 | wa 383 | . 2 wff (𝜑 ∧ 𝜓) |
4 | 2 | wn 3 | . . . 4 wff ¬ 𝜓 |
5 | 1, 4 | wi 4 | . . 3 wff (𝜑 → ¬ 𝜓) |
6 | 5 | wn 3 | . 2 wff ¬ (𝜑 → ¬ 𝜓) |
7 | 3, 6 | wb 195 | 1 wff ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: pm4.63 436 imnan 437 imp 444 ex 449 pm4.54 513 dfbi2 658 pm5.32 666 nfand 1814 nfanOLD 1817 nfan1 2056 nfandOLD 2220 sban 2387 r19.35 3065 dfac5lem4 8832 kmlem3 8857 axrepprim 30833 axunprim 30834 axregprim 30836 axinfprim 30837 axacprim 30838 dfxor4 37077 df3an2 37080 pm11.52 37608 |
Copyright terms: Public domain | W3C validator |