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 108 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | ralimi 2495 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑) |
3 | simpr 109 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | ralimi 2495 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓) |
5 | 2, 4 | jca 304 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
6 | pm3.2 138 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | ral2imi 2497 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
8 | 7 | imp 123 | . 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 125 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∀wral 2416 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 |
This theorem depends on definitions: df-bi 116 df-ral 2421 |
This theorem is referenced by: r19.27v 2559 r19.28v 2560 r19.26-2 2561 r19.26-3 2562 ralbiim 2566 r19.27av 2567 reu8 2880 ssrab 3175 r19.28m 3452 r19.27m 3458 2ralunsn 3725 iuneq2 3829 cnvpom 5081 funco 5163 fncnv 5189 funimaexglem 5206 fnres 5239 fnopabg 5246 mpteqb 5511 eqfnfv3 5520 caoftrn 6007 iinerm 6501 ixpeq2 6606 ixpin 6617 rexanuz 10767 recvguniq 10774 cau3lem 10893 rexanre 10999 bezoutlemmo 11701 sqrt2irr 11847 tgval2 12230 metequiv 12674 metequiv2 12675 mulcncflem 12769 bj-indind 13140 |
Copyright terms: Public domain | W3C validator |