PrintForm
Definitions
elimination
Sections
ClassicalProps(jlc)
Doc
At:
formula
or
right
sound
1
1
1
1.
hyp:
Formula List
2.
M:
Formula List
3.
N:
Formula List
4.
q:
Formula
5.
r:
Formula
6.
a:
Full( < hyp,M @ (q
r.N) > )
a
Full( < hyp,[q; r/ M @ N] > )
By:
AbSetMemEqTypeCD
Generated subgoals:
1
a
Assignment
2
a |= < hyp,[q; r/ M @ N] >
a |
< hyp,[q; r/ M @ N] >
About: