Theorem 19.26 1873

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 483	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1814	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1814	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 512	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1819	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 208	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∀wal 1537

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

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  19.26-2  1874  19.26-3an  1875  19.43OLD  1886  albiim  1892  2albiim  1893  19.27v  1993  19.28v  1994  19.27  2220  19.28  2221  r19.26m  3098  raleqbidvv  3336  unss  4117  ralunb  4124  ssin  4164  falseral0  4450  intun  4911  intprg  4912  intprOLD  4914  eqrelrel  5700  relop  5752  eqoprab2bw  7335  eqoprab2b  7336  dfer2  8486  axgroth4  10598  grothprim  10600  trclfvcotr  14730  caubnd  15080  bj-gl4  34785  bj-nnfand  34939  bj-elgab  35135  wl-alanbii  35732  ax12eq  36963  ax12el  36964  dford4  40859  elmapintrab  41165  elinintrab  41166  ismnuprim  41893  alimp-no-surprise  46463