Theorem 19.26 1798

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

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

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

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

This theorem is referenced by:  19.26-2  1799  19.26-3an  1800  19.43OLD  1811  albiim  1816  2albiim  1817  19.27v  1908  19.28v  1909  19.27  2095  19.28  2096  19.27OLD  2234  19.28OLD  2235  r19.26m  3067  unss  3787  ralunb  3794  ssin  3835  falseral0  4081  intun  4509  intpr  4510  eqrelrel  5221  relop  5272  eqoprab2b  6713  dfer2  7743  axgroth4  9654  grothprim  9656  trclfvcotr  13750  caubnd  14098  bj-gl4lem  32579  bj-gl4  32580  wl-alanbii  33351  ax12eq  34226  ax12el  34227  dford4  37596  elmapintrab  37882  elinintrab  37883  alimp-no-surprise  42527