![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.26 | Structured version Visualization version GIF version |
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
19.26 | ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 476 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | alimi 1910 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑) |
3 | simpr 479 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | alimi 1910 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓) |
5 | 2, 4 | jca 507 | . 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
6 | id 22 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
7 | 6 | alanimi 1915 | . 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) |
8 | 5, 7 | impbii 201 | 1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∀wal 1654 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 |
This theorem depends on definitions: df-bi 199 df-an 387 |
This theorem is referenced by: 19.26-2 1973 19.26-3an 1974 19.26-3anOLD 1975 19.43OLD 1986 albiim 1991 2albiim 1992 19.27v 2094 19.28v 2095 19.27 2270 19.28 2271 eu6OLD 2647 r19.26m 3277 unss 4016 ralunb 4023 ssin 4061 falseral0 4303 intun 4731 intpr 4732 eqrelrel 5459 relop 5509 eqoprab2b 6978 dfer2 8015 axgroth4 9976 grothprim 9978 trclfvcotr 14134 caubnd 14482 bj-gl4lem 33103 bj-gl4 33104 wl-alanbii 33894 ax12eq 35015 ax12el 35016 dford4 38438 elmapintrab 38722 elinintrab 38723 alimp-no-surprise 43437 |
Copyright terms: Public domain | W3C validator |