BoxImpNow

f f BoxImpNow

Proof:

1
¬f ¬f
2
¬¬f f
1,Prop
3
f f
2, def. of 

qed

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023