Theorem 19.26 1902

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

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

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

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

This theorem is used by:  19.26-2  1903  19.26-3an  1904  19.43OLD  1915  albiim  1921  2albiim  1922  19.27v  2027  19.28v  2028  19.27  2263  19.28  2264  r19.26m  3121  ssin  4134  unss  4187  ralunb  4194  falseral0OLD  4470  intun  4939  intprg  4940  eqrelrel  5774  relop  5829  eqoprab2bw  7494  eqoprab2b  7495  dfer2  8726  axgroth4  10924  grothprim  10926  trclfvcotr  15171  caubnd  15535  mh-prprimbi  37455  mh-infprim1bi  37458  bj-gl4  37589  bj-nnfand  37781  bj-elgab  37976  bj-axreprepsep  38127  wl-alanbii  38638  ax12eq  40135  ax12el  40136  alan  43814  dford4  44173  elmapintrab  44714  elinintrab  44715  ismnuprim  45415  alimp-no-surprise  51088