Theorem 19.26 1065

Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119.

Assertion

Ref	Expression
19.26	⊢ (∀x(φ ⋀ ψ) ↔ (∀xφ ⋀ ∀xψ))

Proof of Theorem 19.26

Step	Hyp	Ref	Expression
1		pm3.26 319	. . . 4 ⊢ ((φ ⋀ ψ) → φ)
2	1	19.20i 990	. . 3 ⊢ (∀x(φ ⋀ ψ) → ∀xφ)
3		pm3.27 323	. . . 4 ⊢ ((φ ⋀ ψ) → ψ)
4	3	19.20i 990	. . 3 ⊢ (∀x(φ ⋀ ψ) → ∀xψ)
5	2, 4	jca 288	. 2 ⊢ (∀x(φ ⋀ ψ) → (∀xφ ⋀ ∀xψ))
6		pm3.2 283	. . . 4 ⊢ (φ → (ψ → (φ ⋀ ψ)))
7	6	19.20ii 993	. . 3 ⊢ (∀xφ → (∀xψ → ∀x(φ ⋀ ψ)))
8	7	imp 350	. 2 ⊢ ((∀xφ ⋀ ∀xψ) → ∀x(φ ⋀ ψ))
9	5, 8	impbi 157	1 ⊢ (∀x(φ ⋀ ψ) ↔ (∀xφ ⋀ ∀xψ))

Syntax hints:   ↔ wb 146   ⋀ wa 223  ∀wal 952

This theorem is referenced by:  19.26-2 1066  19.27 1067  19.28 1068  19.35 1073  19.43 1086  albi 1105  2albi 1106  hband 1109  a4imed 1159  ax11eq 1361  ax11el 1362  a12stdy2 1371  a12lem1 1374  2eu4 1450  bm1.1 1460  r19.26 1747  r19.26m 1749  unss 2200  ralpr 2424  prsspw 2476  intun 2557  intpr 2558  bm1.3ii 2701  relop 3270  asymref2 3432  dfer2 4252  suppsr3 5204  pre-axsup 5271  axgroth4 8719  grothprim 8722

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain