Theorem 19.26 1948

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 468	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1886	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 471	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1886	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 495	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1891	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 199	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 382  ∀wal 1628

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

This theorem depends on definitions:  df-bi 197  df-an 383

This theorem is referenced by:  19.26-2  1949  19.26-3an  1950  19.26-3anOLD  1951  19.43OLD  1962  albiim  1967  2albiim  1968  19.27v  2075  19.28v  2076  19.27  2250  19.28  2251  19.27OLD  2395  19.28OLD  2396  r19.26m  3214  unss  3936  ralunb  3943  ssin  3981  falseral0  4218  intun  4641  intpr  4642  eqrelrel  5361  relop  5411  eqoprab2b  6859  dfer2  7896  axgroth4  9855  grothprim  9857  trclfvcotr  13957  caubnd  14305  bj-gl4lem  32910  bj-gl4  32911  wl-alanbii  33678  ax12eq  34742  ax12el  34743  dford4  38115  elmapintrab  38401  elinintrab  38402  alimp-no-surprise  43048