![]() |
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 468 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | alimi 1886 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑) |
3 | simpr 471 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | alimi 1886 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓) |
5 | 2, 4 | jca 495 | . 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
6 | id 22 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
7 | 6 | alanimi 1891 | . 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) |
8 | 5, 7 | impbii 199 | 1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 ∀wal 1628 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 |
This theorem depends on definitions: df-bi 197 df-an 383 |
This theorem is referenced by: 19.26-2 1949 19.26-3an 1950 19.26-3anOLD 1951 19.43OLD 1962 albiim 1967 2albiim 1968 19.27v 2075 19.28v 2076 19.27 2250 19.28 2251 19.27OLD 2395 19.28OLD 2396 r19.26m 3214 unss 3936 ralunb 3943 ssin 3981 falseral0 4218 intun 4641 intpr 4642 eqrelrel 5361 relop 5411 eqoprab2b 6859 dfer2 7896 axgroth4 9855 grothprim 9857 trclfvcotr 13957 caubnd 14305 bj-gl4lem 32910 bj-gl4 32911 wl-alanbii 33678 ax12eq 34742 ax12el 34743 dford4 38115 elmapintrab 38401 elinintrab 38402 alimp-no-surprise 43048 |
Copyright terms: Public domain | W3C validator |