Theorem 19.26 1877

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 1818	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1818	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 516	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1823	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 210	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∀wal 1545

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  19.26-2  1878  19.26-3an  1879  19.43OLD  1890  albiim  1896  2albiim  1897  19.27v  2002  19.28v  2003  19.27  2239  19.28  2240  r19.26m  3098  unss  4119  ralunb  4126  ssin  4167  falseral0OLD  4443  intun  4910  intprg  4911  eqrelrel  5740  relop  5792  eqoprab2bw  7426  eqoprab2b  7427  dfer2  8634  axgroth4  10746  grothprim  10748  trclfvcotr  14962  caubnd  15312  mh-prprimbi  36771  mh-infprim1bi  36774  bj-gl4  36906  bj-nnfand  37098  bj-elgab  37292  bj-axreprepsep  37428  wl-alanbii  37940  ax12eq  39433  ax12el  39434  alan  43116  dford4  43474  elmapintrab  44020  elinintrab  44021  ismnuprim  44738  alimp-no-surprise  50271