Next
Prev
Up
LeftChopChopImpChopRule
⊢
f
;
g
⊃
g
⇒ ⊢
f
;
g
;
h
⊃
g
;
h
LeftChopChopImpChopRule
Proof:
1
⊢
f
;
g
⊃
g
given
2
⊢
(
f
;
g
) ;
h
⊃
g
;
h
1
,
LeftChopImpChop
3
⊢
(
f
;
g
) ;
h
≡
f
;
g
;
h
ChopAssoc
4
⊢
f
;
g
;
h
⊃
g
;
h
2
,
3
,
Prop
qed
Next
Prev
Up
2023-09-12
Contact
|
Home
|
ITL home
|
Course
|
Proofs
|
Algebra
|
FL
© 1996-2023