![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.26 | GIF version |
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
19.26 | ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | alimi 1412 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑) |
3 | simpr 109 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | alimi 1412 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓) |
5 | 2, 4 | jca 302 | . 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
6 | id 19 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
7 | 6 | alanimi 1416 | . 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) |
8 | 5, 7 | impbii 125 | 1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∀wal 1310 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.26-2 1439 19.26-3an 1440 albiim 1444 2albiim 1445 hband 1446 hban 1507 19.27h 1520 19.27 1521 19.28h 1522 19.28 1523 nford 1527 nfand 1528 equsexd 1688 equveli 1713 sbanv 1841 2eu4 2066 bm1.1 2098 r19.26m 2535 unss 3214 ralunb 3221 ssin 3262 intun 3766 intpr 3767 eqrelrel 4598 relop 4647 eqoprab2b 5781 dfer2 6382 |
Copyright terms: Public domain | W3C validator |