Theorem 19.26 1796

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 473	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1737	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 477	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1737	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 554	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1742	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 199	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 384  ∀wal 1479

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

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

This theorem is referenced by:  19.26-2  1797  19.26-3an  1798  19.43OLD  1809  albiim  1814  2albiim  1815  19.27v  1906  19.28v  1907  19.27  2093  19.28  2094  19.27OLD  2232  19.28OLD  2233  r19.26m  3063  unss  3779  ralunb  3786  ssin  3827  falseral0  4072  intun  4500  intpr  4501  eqrelrel  5211  relop  5261  eqoprab2b  6698  dfer2  7728  axgroth4  9639  grothprim  9641  trclfvcotr  13731  caubnd  14079  bj-gl4lem  32554  bj-gl4  32555  wl-alanbii  33322  ax12eq  34045  ax12el  34046  dford4  37415  elmapintrab  37701  elinintrab  37702  alimp-no-surprise  42292