Theorem 19.26 1868

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 482	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1808	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1808	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 511	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1813	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1535

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  19.26-2  1869  19.26-3an  1870  19.43OLD  1881  albiim  1887  2albiim  1888  19.27v  1987  19.28v  1988  19.27  2225  19.28  2226  r19.26m  3108  raleqbidvvOLD  3333  unss  4200  ralunb  4207  ssin  4247  falseral0  4522  intun  4985  intprg  4986  eqrelrel  5810  relop  5864  eqoprab2bw  7503  eqoprab2b  7504  dfer2  8745  axgroth4  10870  grothprim  10872  trclfvcotr  15045  caubnd  15394  bj-gl4  36578  bj-nnfand  36732  bj-elgab  36922  wl-alanbii  37550  ax12eq  38923  ax12el  38924  alan  42653  dford4  43018  elmapintrab  43566  elinintrab  43567  ismnuprim  44290  alimp-no-surprise  49012