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 486	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1813	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1813	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 515	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1818	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∀wal 1536

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

This theorem depends on definitions:  df-bi 210  df-an 400

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  2227  19.28  2228  r19.26m  3140  unss  4111  ralunb  4118  ssin  4157  falseral0  4417  intun  4870  intpr  4871  eqrelrel  5634  relop  5685  eqoprab2bw  7203  eqoprab2b  7204  dfer2  8273  axgroth4  10243  grothprim  10245  trclfvcotr  14360  caubnd  14710  bj-gl4  34042  bj-nnfand  34193  wl-alanbii  34970  ax12eq  36237  ax12el  36238  dford4  39970  elmapintrab  40276  elinintrab  40277  ismnuprim  41002  alimp-no-surprise  45309