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  3338  unss  4118  ralunb  4125  ssin  4164  falseral0  4450  intun  4911  intprg  4912  intprOLD  4914  eqrelrel  5707  relop  5759  eqoprab2bw  7345  eqoprab2b  7346  dfer2  8499  axgroth4  10588  grothprim  10590  trclfvcotr  14720  caubnd  15070  bj-gl4  34777  bj-nnfand  34931  bj-elgab  35127  wl-alanbii  35724  ax12eq  36955  ax12el  36956  dford4  40851  elmapintrab  41184  elinintrab  41185  ismnuprim  41912  alimp-no-surprise  46485