Theorem 19.26 1874

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 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1814	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 486	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1814	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 513	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1819	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 208	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397  ∀wal 1540

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

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  19.26-2  1875  19.26-3an  1876  19.43OLD  1887  albiim  1893  2albiim  1894  19.27v  1994  19.28v  1995  19.27  2221  19.28  2222  r19.26m  3111  raleqbidvvOLD  3331  unss  4183  ralunb  4190  ssin  4229  falseral0  4518  intun  4983  intprg  4984  intprOLD  4986  eqrelrel  5795  relop  5848  eqoprab2bw  7474  eqoprab2b  7475  dfer2  8700  axgroth4  10823  grothprim  10825  trclfvcotr  14952  caubnd  15301  bj-gl4  35411  bj-nnfand  35565  bj-elgab  35757  wl-alanbii  36372  ax12eq  37749  ax12el  37750  dford4  41701  elmapintrab  42260  elinintrab  42261  ismnuprim  42986  alimp-no-surprise  47730