| 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 482 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
| 2 | 1 | alimi 1811 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑) |
| 3 | simpr 484 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
| 4 | 3 | alimi 1811 | . . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓) |
| 5 | 2, 4 | jca 511 | . 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
| 6 | id 22 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
| 7 | 6 | alanimi 1816 | . 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) |
| 8 | 5, 7 | impbii 209 | 1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: 19.26-2 1871 19.26-3an 1872 19.43OLD 1883 albiim 1889 2albiim 1890 19.27v 1989 19.28v 1990 19.27 2227 19.28 2228 r19.26m 3110 raleqbidvvOLD 3335 unss 4190 ralunb 4197 ssin 4239 falseral0 4516 intun 4980 intprg 4981 eqrelrel 5807 relop 5861 eqoprab2bw 7503 eqoprab2b 7504 dfer2 8746 axgroth4 10872 grothprim 10874 trclfvcotr 15048 caubnd 15397 bj-gl4 36596 bj-nnfand 36750 bj-elgab 36940 wl-alanbii 37570 ax12eq 38942 ax12el 38943 alan 42676 dford4 43041 elmapintrab 43589 elinintrab 43590 ismnuprim 44313 alimp-no-surprise 49300 |
| Copyright terms: Public domain | W3C validator |