Theorem 19.26 1903

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 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1844	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1844	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 521	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 23	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1849	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  19.26-2  1904  19.26-3an  1905  19.43OLD  1918  albiim  1924  2albiim  1925  19.27v  2030  19.28v  2031  19.27  2267  19.28  2268  r19.26m  3125  ssin  4138  unss  4191  ralunb  4198  falseral0OLD  4474  intun  4945  intprg  4946  eqrelrel  5782  relop  5838  eqoprab2bw  7521  eqoprab2b  7522  dfer2  8756  axgroth4  10956  grothprim  10958  trclfvcotr  15205  caubnd  15570  mh-prprimbi  37546  mh-infprim1bi  37549  bj-gl4  37680  bj-nnfand  37872  bj-elgab  38067  bj-axreprepsep  38261  wl-alanbii  38769  ax12eq  40264  ax12el  40265  alan  43943  dford4  44302  elmapintrab  44838  elinintrab  44839  ismnuprim  45539  alimp-no-surprise  51305