P. 168 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16701-16701   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	alsc2d 16701	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( ph -> A.! x e. A ps )   =>    |- ( ph -> E. x x e. A )

< Previous  Wrap >