Theorem 19.26 1411

Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-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 107	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1385	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 108	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1385	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 300	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 19	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1389	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 124	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ∧ wa 102   ↔ wb 103  ∀wal 1283

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.26-2  1412  19.26-3an  1413  albiim  1417  2albiim  1418  hband  1419  hban  1480  19.27h  1493  19.27  1494  19.28h  1495  19.28  1496  nford  1500  nfand  1501  equsexd  1658  equveli  1683  sbanv  1811  2eu4  2035  bm1.1  2067  r19.26m  2489  unss  3147  ralunb  3154  ssin  3189  intun  3669  intpr  3670  eqrelrel  4461  relop  4508  eqoprab2b  5588  dfer2  6166