Kui meil õnnestub tõestada, et täiendatud eelduste komplektist saab tuletada konditsionaali tagajärje (G, p ⊢ q), siis sellest saab loogiliselt järeldada (formaalne implikatsioon ⇒), et algsest eelduste komplektist G saab tuletada tingiva väite p → q, valemina G, p ⊢ q ⇒G ⊢ (p → q). Täiendavat eeldust p nimetatakse hüpoteesiks ning neid võib olla ka mitu. Eelduste hulka G võib vaadelda kui lausetesüsteemi {r1, r2, ... , rn}. Tingimusliku tõestuse lubatavus järeldub ekvivalentsusseosest: [(r1 & r2 & … & rn) → (p → q)] ↔ (r1 & r2 & … & rn & p) → q. Tingimusliku (konditsionaalse) tõestuse puhul sisaldab tuletuse jada lõike, mis sõltuvad lisaks üldistele eeldustele ka hüpoteesist p kui täiendavast eeldusest. Sellist lõiku nimetatakse alamtuletuseks ning seda tähistatakse püstjoonega vasakul pool. Alamtuletuse sees võib olla veel täiendavaid alamtuletusi. Need tähistatakse täiendava joonega valemitest vasakul, ent peamisest joonest paremal pool
Kui meil õnnestub tõestada, et täiendatud eelduste komplektist saab tuletada konditsionaali tagajärje (G, p q), siis sellest saab loogiliselt järeldada (formaalne implikatsioon ), et algsest eelduste komplektist G saab tuletada tingiva väite p q, valemina G, p q G (p q). Täiendavat eeldust p nimetatakse hüpoteesiks ning neid võib olla ka mitu. Eelduste hulka G võib vaadelda kui lausetesüsteemi {r1, r2, ... , rn}. Tingimusliku tõestuse lubatavus järeldub ekvivalentsusseosest: [(r1 & r2 & ... & rn) (p q)] (r1 & r2 & ... & rn & p) q. Tingimusliku (konditsionaalse) tõestuse puhul sisaldab tuletuse jada lõike, mis sõltuvad lisaks üldistele eeldustele ka hüpoteesist p kui täiendavast eeldusest. Sellist lõiku nimetatakse alamtuletuseks ning seda tähistatakse püstjoonega vasakul pool. Alamtuletuse sees võib olla veel täiendavaid alamtuletusi. Need tähistatakse täiendava joonega valemitest vasakul, ent peamisest joonest paremal pool
annaabi.ee 
