...

Док-во от противного также называют еще modus tollens.

На входе:
(если A то B) - истинно
(B) - ложно
На выходе:
(A) - ложно

А для чисто истинных есть modus ponens:

На входе:
(если A то B) - истинно
(A) - истинно
На выходе:
(B) - истинно

При этом многие правила можно юзать рекурсивно, по схеме: если где-то когда-то на входе было A, а на выходе B, то тем самым доказано:
"если A то B" - истинно.