![]() |
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 472 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | alimi 1779 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑) |
3 | simpr 476 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | alimi 1779 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓) |
5 | 2, 4 | jca 553 | . 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
6 | id 22 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
7 | 6 | alanimi 1784 | . 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) |
8 | 5, 7 | impbii 199 | 1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∀wal 1521 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: 19.26-2 1839 19.26-3an 1840 19.43OLD 1851 albiim 1856 2albiim 1857 19.27v 1964 19.28v 1965 19.27 2133 19.28 2134 19.27OLD 2270 19.28OLD 2271 r19.26m 3096 unss 3820 ralunb 3827 ssin 3868 falseral0 4114 intun 4541 intpr 4542 eqrelrel 5255 relop 5305 eqoprab2b 6755 dfer2 7788 axgroth4 9692 grothprim 9694 trclfvcotr 13794 caubnd 14142 bj-gl4lem 32704 bj-gl4 32705 wl-alanbii 33481 ax12eq 34545 ax12el 34546 dford4 37913 elmapintrab 38199 elinintrab 38200 alimp-no-surprise 42855 |
Copyright terms: Public domain | W3C validator |