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  7483  eqoprab2b  7484  dfer2  8697  axgroth4  10841  grothprim  10843  trclfvcotr  15082  caubnd  15446  mh-prprimbi  37162  mh-infprim1bi  37165  bj-gl4  37296  bj-nnfand  37488  bj-elgab  37683  bj-axreprepsep  37820  wl-alanbii  38332  ax12eq  39814  ax12el  39815  alan  43512  dford4  43870  elmapintrab  44416  elinintrab  44417  ismnuprim  45118  alimp-no-surprise  50710