Theorem 19.26 1869

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

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

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

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

This theorem is referenced by:  19.26-2  1870  19.26-3an  1871  19.43OLD  1882  albiim  1888  2albiim  1889  19.27v  1989  19.28v  1990  19.27  2228  19.28  2229  r19.26m  3116  raleqbidvvOLD  3343  unss  4213  ralunb  4220  ssin  4260  falseral0  4539  intun  5004  intprg  5005  eqrelrel  5821  relop  5875  eqoprab2bw  7520  eqoprab2b  7521  dfer2  8764  axgroth4  10901  grothprim  10903  trclfvcotr  15058  caubnd  15407  bj-gl4  36561  bj-nnfand  36715  bj-elgab  36905  wl-alanbii  37523  ax12eq  38897  ax12el  38898  alan  42621  dford4  42986  elmapintrab  43538  elinintrab  43539  ismnuprim  44263  alimp-no-surprise  48875