Theorem 19.26 1890

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 486	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1831	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1831	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 519	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1836	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 211	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 399  ∀wal 1558

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  19.26-2  1891  19.26-3an  1892  19.43OLD  1903  albiim  1909  2albiim  1910  19.27v  2015  19.28v  2016  19.27  2262  19.28  2263  r19.26m  3121  unss  4142  ralunb  4149  ssin  4190  falseral0OLD  4469  intun  4938  intprg  4939  eqrelrel  5769  relop  5822  eqoprab2bw  7466  eqoprab2b  7467  dfer2  8679  axgroth4  10790  grothprim  10792  trclfvcotr  15022  caubnd  15386  mh-prprimbi  36903  mh-infprim1bi  36906  bj-gl4  37038  bj-nnfand  37230  bj-elgab  37424  bj-axreprepsep  37560  wl-alanbii  38072  ax12eq  39565  ax12el  39566  alan  43248  dford4  43606  elmapintrab  44152  elinintrab  44153  ismnuprim  44870  alimp-no-surprise  50402