Theorem 19.26 1871

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

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

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

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

This theorem is referenced by:  19.26-2  1872  19.26-3an  1873  19.43OLD  1884  albiim  1890  2albiim  1891  19.27v  1996  19.28v  1997  19.27  2230  19.28  2231  r19.26m  3091  raleqbidvvOLD  3301  unss  4137  ralunb  4144  ssin  4186  falseral0  4463  intun  4928  intprg  4929  eqrelrel  5736  relop  5789  eqoprab2bw  7416  eqoprab2b  7417  dfer2  8623  axgroth4  10723  grothprim  10725  trclfvcotr  14916  caubnd  15266  bj-gl4  36637  bj-nnfand  36791  bj-elgab  36981  wl-alanbii  37611  ax12eq  38988  ax12el  38989  alan  42707  dford4  43070  elmapintrab  43617  elinintrab  43618  ismnuprim  44335  alimp-no-surprise  49821