Theorem 19.26 1972

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 476	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1910	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 479	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1910	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 507	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1915	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 201	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 386  ∀wal 1654

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

This theorem depends on definitions:  df-bi 199  df-an 387

This theorem is referenced by:  19.26-2  1973  19.26-3an  1974  19.26-3anOLD  1975  19.43OLD  1986  albiim  1991  2albiim  1992  19.27v  2094  19.28v  2095  19.27  2270  19.28  2271  eu6OLD  2647  r19.26m  3277  unss  4016  ralunb  4023  ssin  4061  falseral0  4303  intun  4731  intpr  4732  eqrelrel  5459  relop  5509  eqoprab2b  6978  dfer2  8015  axgroth4  9976  grothprim  9978  trclfvcotr  14134  caubnd  14482  bj-gl4lem  33103  bj-gl4  33104  wl-alanbii  33894  ax12eq  35015  ax12el  35016  dford4  38438  elmapintrab  38722  elinintrab  38723  alimp-no-surprise  43437