Theorem 19.26 1897

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 1838	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1838	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 520	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 23	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1843	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

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

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

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

This theorem is referenced by:  19.26-2  1898  19.26-3an  1899  19.43OLD  1910  albiim  1916  2albiim  1917  19.27v  2022  19.28v  2023  19.27  2269  19.28  2270  r19.26m  3130  unss  4151  ralunb  4158  ssin  4199  falseral0OLD  4481  intun  4949  intprg  4950  eqrelrel  5784  relop  5837  eqoprab2bw  7481  eqoprab2b  7482  dfer2  8694  axgroth4  10816  grothprim  10818  trclfvcotr  15045  caubnd  15409  mh-prprimbi  36942  mh-infprim1bi  36945  bj-gl4  37076  bj-nnfand  37268  bj-elgab  37462  bj-axreprepsep  37599  wl-alanbii  38111  ax12eq  39604  ax12el  39605  alan  43289  dford4  43647  elmapintrab  44193  elinintrab  44194  ismnuprim  44895  alimp-no-surprise  50443