Theorem 19.26 1872

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 482	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1813	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1813	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 511	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1818	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1540

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  19.26-2  1873  19.26-3an  1874  19.43OLD  1885  albiim  1891  2albiim  1892  19.27v  1997  19.28v  1998  19.27  2235  19.28  2236  r19.26m  3097  unss  4131  ralunb  4138  ssin  4180  falseral0OLD  4456  intun  4923  intprg  4924  eqrelrel  5747  relop  5800  eqoprab2bw  7431  eqoprab2b  7432  dfer2  8638  axgroth4  10749  grothprim  10751  trclfvcotr  14965  caubnd  15315  mh-prprimbi  36744  mh-infprim1bi  36747  bj-gl4  36879  bj-nnfand  37071  bj-elgab  37265  bj-axreprepsep  37401  wl-alanbii  37911  ax12eq  39404  ax12el  39405  alan  43116  dford4  43478  elmapintrab  44024  elinintrab  44025  ismnuprim  44742  alimp-no-surprise  50271