Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Andrew Salmon
Principia Mathematica * 10
pm10.56
Next ⟩
pm10.57
Metamath Proof Explorer
Ascii
Unicode
Theorem
pm10.56
Description:
Theorem *10.56 in
WhiteheadRussell
p. 156.
(Contributed by
Andrew Salmon
, 24-May-2011)
Ref
Expression
Assertion
pm10.56
⊢
∀
x
φ
→
ψ
∧
∃
x
φ
∧
χ
→
∃
x
ψ
∧
χ
Proof
Step
Hyp
Ref
Expression
1
pm3.45
⊢
φ
→
ψ
→
φ
∧
χ
→
ψ
∧
χ
2
1
aleximi
⊢
∀
x
φ
→
ψ
→
∃
x
φ
∧
χ
→
∃
x
ψ
∧
χ
3
2
imp
⊢
∀
x
φ
→
ψ
∧
∃
x
φ
∧
χ
→
∃
x
ψ
∧
χ