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  3096  unss  4130  ralunb  4137  ssin  4179  falseral0OLD  4455  intun  4922  intprg  4923  eqrelrel  5753  relop  5805  eqoprab2bw  7437  eqoprab2b  7438  dfer2  8644  axgroth4  10755  grothprim  10757  trclfvcotr  14971  caubnd  15321  mh-prprimbi  36725  mh-infprim1bi  36728  bj-gl4  36860  bj-nnfand  37052  bj-elgab  37246  bj-axreprepsep  37382  wl-alanbii  37894  ax12eq  39387  ax12el  39388  alan  43099  dford4  43457  elmapintrab  44003  elinintrab  44004  ismnuprim  44721  alimp-no-surprise  50256