![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > r19.26 | GIF version |
Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
r19.26 | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 107 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | ralimi 2427 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑) |
3 | simpr 108 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | ralimi 2427 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓) |
5 | 2, 4 | jca 300 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
6 | pm3.2 137 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | ral2imi 2428 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
8 | 7 | imp 122 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 124 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 ∀wral 2349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 |
This theorem depends on definitions: df-bi 115 df-ral 2354 |
This theorem is referenced by: r19.26-2 2487 r19.26-3 2488 ralbiim 2492 r19.27av 2493 reu8 2789 ssrab 3073 r19.28m 3332 r19.27m 3338 2ralunsn 3592 iuneq2 3696 cnvpom 4884 funco 4964 fncnv 4990 funimaexglem 5007 fnres 5040 fnopabg 5047 mpteqb 5287 eqfnfv3 5293 caoftrn 5761 iinerm 6237 rexanuz 10001 recvguniq 10008 cau3lem 10127 rexanre 10233 bezoutlemmo 10528 sqrt2irr 10674 bj-indind 10870 |
Copyright terms: Public domain | W3C validator |