![]() |
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 109 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | alimi 1466 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑) |
3 | simpr 110 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | alimi 1466 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓) |
5 | 2, 4 | jca 306 | . 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
6 | id 19 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
7 | 6 | alanimi 1470 | . 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) |
8 | 5, 7 | impbii 126 | 1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 ∀wal 1362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 19.26-2 1493 19.26-3an 1494 albiim 1498 2albiim 1499 hband 1500 hban 1558 19.27h 1571 19.27 1572 19.28h 1573 19.28 1574 nford 1578 nfand 1579 equsexd 1740 equveli 1770 sbanv 1901 2eu4 2131 bm1.1 2174 r19.26m 2621 unss 3324 ralunb 3331 ssin 3372 intun 3890 intpr 3891 eqrelrel 4745 relop 4795 eqoprab2b 5955 dfer2 6561 omniwomnimkv 7196 |
Copyright terms: Public domain | W3C validator |