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  2234  19.28  2235  r19.26m  3095  raleqbidvvOLD  3305  unss  4142  ralunb  4149  ssin  4191  falseral0OLD  4468  intun  4935  intprg  4936  eqrelrel  5746  relop  5799  eqoprab2bw  7428  eqoprab2b  7429  dfer2  8636  axgroth4  10743  grothprim  10745  trclfvcotr  14932  caubnd  15282  bj-gl4  36795  bj-nnfand  36950  bj-elgab  37140  wl-alanbii  37774  ax12eq  39201  ax12el  39202  alan  42909  dford4  43271  elmapintrab  43817  elinintrab  43818  ismnuprim  44535  alimp-no-surprise  50026