Theorem 19.26 1866

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

Syntax hints:   ↔ wb 205   ∧ wa 394  ∀wal 1532

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

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

This theorem is referenced by:  19.26-2  1867  19.26-3an  1868  19.43OLD  1879  albiim  1885  2albiim  1886  19.27v  1986  19.28v  1987  19.27  2216  19.28  2217  r19.26m  3100  raleqbidvvOLD  3320  unss  4182  ralunb  4189  ssin  4229  falseral0  4514  intun  4980  intprg  4981  intprOLD  4983  eqrelrel  5795  relop  5849  eqoprab2bw  7487  eqoprab2b  7488  dfer2  8727  axgroth4  10866  grothprim  10868  trclfvcotr  15009  caubnd  15358  bj-gl4  36313  bj-nnfand  36467  bj-elgab  36658  wl-alanbii  37277  ax12eq  38652  ax12el  38653  dford4  42724  elmapintrab  43280  elinintrab  43281  ismnuprim  44005  alimp-no-surprise  48565