Theorem 19.26 1838

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 472	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1779	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 476	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1779	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 553	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1784	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 199	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 383  ∀wal 1521

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

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

This theorem is referenced by:  19.26-2  1839  19.26-3an  1840  19.43OLD  1851  albiim  1856  2albiim  1857  19.27v  1964  19.28v  1965  19.27  2133  19.28  2134  19.27OLD  2270  19.28OLD  2271  r19.26m  3096  unss  3820  ralunb  3827  ssin  3868  falseral0  4114  intun  4541  intpr  4542  eqrelrel  5255  relop  5305  eqoprab2b  6755  dfer2  7788  axgroth4  9692  grothprim  9694  trclfvcotr  13794  caubnd  14142  bj-gl4lem  32704  bj-gl4  32705  wl-alanbii  33481  ax12eq  34545  ax12el  34546  dford4  37913  elmapintrab  38199  elinintrab  38200  alimp-no-surprise  42855