Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Andrew Salmon
Principia Mathematica * 10
pm10.52
Next ⟩
pm10.53
Metamath Proof Explorer
Ascii
Unicode
Theorem
pm10.52
Description:
Theorem *10.52 in
WhiteheadRussell
p. 155.
(Contributed by
Andrew Salmon
, 24-May-2011)
Ref
Expression
Assertion
pm10.52
⊢
∃
x
φ
→
∀
x
φ
→
ψ
↔
ψ
Proof
Step
Hyp
Ref
Expression
1
19.23v
⊢
∀
x
φ
→
ψ
↔
∃
x
φ
→
ψ
2
pm5.5
⊢
∃
x
φ
→
∃
x
φ
→
ψ
↔
ψ
3
1
2
syl5bb
⊢
∃
x
φ
→
∀
x
φ
→
ψ
↔
ψ