Theorem 19.26 1786

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 472	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1730	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 476	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1730	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 553	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 22	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1734	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 198	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383  ∀wal 1473

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  19.26-2  1787  19.26-3an  1788  19.43OLD  1800  albiim  1806  2albiim  1807  19.27v  1895  19.28v  1896  19.27  2082  19.28  2083  19.27OLD  2222  19.28OLD  2223  r19.26m  3049  unss  3749  ralunb  3756  ssin  3797  intun  4439  intpr  4440  eqrelrel  5133  relop  5182  eqoprab2b  6589  dfer2  7608  axgroth4  9511  grothprim  9513  trclfvcotr  13547  caubnd  13895  bj-gl4lem  31546  bj-gl4  31547  wl-alanbii  32324  ax12eq  33038  ax12el  33039  dford4  36408  elmapintrab  36695  elinintrab  36696  falseral0  40103  alimp-no-surprise  42289