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  1916  albiim  1922  2albiim  1923  19.27v  2028  19.28v  2029  19.27  2266  19.28  2267  r19.26m  3126  unss  4143  ralunb  4150  ssin  4191  falseral0OLD  4478  intun  4947  intprg  4948  eqrelrel  5785  relop  5838  eqoprab2bw  7489  eqoprab2b  7490  dfer2  8701  axgroth4  10832  grothprim  10834  trclfvcotr  15070  caubnd  15434  mh-prprimbi  37111  mh-infprim1bi  37114  bj-gl4  37245  bj-nnfand  37437  bj-elgab  37632  bj-axreprepsep  37769  wl-alanbii  38281  ax12eq  39773  ax12el  39774  alan  43456  dford4  43814  elmapintrab  44360  elinintrab  44361  ismnuprim  45062  alimp-no-surprise  50616