Theorem 19.26 1900

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.)

Assertion

Ref	Expression
19.26	⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Proof of Theorem 19.26

Step	Hyp	Ref	Expression
1		simpl 487	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1841	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1841	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 520	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 23	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1846	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∀wal 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  19.26-2  1901  19.26-3an  1902  19.43OLD  1913  albiim  1919  2albiim  1920  19.27v  2025  19.28v  2026  19.27  2263  19.28  2264  r19.26m  3124  unss  4143  ralunb  4150  ssin  4191  falseral0OLD  4476  intun  4945  intprg  4946  eqrelrel  5783  relop  5836  eqoprab2bw  7480  eqoprab2b  7481  dfer2  8691  axgroth4  10812  grothprim  10814  trclfvcotr  15042  caubnd  15406  mh-prprimbi  37054  mh-infprim1bi  37057  bj-gl4  37188  bj-nnfand  37380  bj-elgab  37575  bj-axreprepsep  37712  wl-alanbii  38224  ax12eq  39715  ax12el  39716  alan  43398  dford4  43756  elmapintrab  44302  elinintrab  44303  ismnuprim  45004  alimp-no-surprise  50559