Theorem 19.26 1903

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 488	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	alimi 1844	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜑)
3		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	alimi 1844	. . 3 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → ∀𝑥𝜓)
5	2, 4	jca 521	. 2 ⊢ (∀𝑥(𝜑 ∧ 𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6		id 23	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
7	6	alanimi 1849	. 2 ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
8	5, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  19.26-2  1904  19.26-3an  1905  19.43OLD  1916  albiim  1922  2albiim  1923  19.27v  2028  19.28v  2029  19.27  2263  19.28  2264  r19.26m  3121  unss  4136  ralunb  4143  ssin  4184  falseral0OLD  4471  intun  4940  intprg  4941  eqrelrel  5777  relop  5830  eqoprab2bw  7484  eqoprab2b  7485  dfer2  8698  axgroth4  10842  grothprim  10844  trclfvcotr  15083  caubnd  15447  mh-prprimbi  37163  mh-infprim1bi  37166  bj-gl4  37297  bj-nnfand  37489  bj-elgab  37684  bj-axreprepsep  37821  wl-alanbii  38333  ax12eq  39815  ax12el  39816  alan  43513  dford4  43871  elmapintrab  44417  elinintrab  44418  ismnuprim  45119  alimp-no-surprise  50711