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  2264  19.28  2265  r19.26m  3122  unss  4136  ralunb  4143  ssin  4184  falseral0OLD  4471  intun  4940  intprg  4941  eqrelrel  5773  relop  5828  eqoprab2bw  7490  eqoprab2b  7491  dfer2  8718  axgroth4  10917  grothprim  10919  trclfvcotr  15162  caubnd  15526  mh-prprimbi  37331  mh-infprim1bi  37334  bj-gl4  37465  bj-nnfand  37657  bj-elgab  37852  bj-axreprepsep  37991  wl-alanbii  38501  ax12eq  39998  ax12el  39999  alan  43677  dford4  44035  elmapintrab  44576  elinintrab  44577  ismnuprim  45277  alimp-no-surprise  50876