Nechť proměnná x není volná ve formuli B a nechť |- A→B
Potom |- (∃x)A→B
Předpoklad je
|- A→B
Dle v5 výrokové logiky (a tedy zároveň predikátové) a modus ponens
A->B (A->B)->(¬B->¬A) --------------------------- ¬B->¬A
|- ¬B→¬A
Dále použiju pravidlo zavední obecného kvantifikátoru a v4 výrokové logiky (s tou v4 si nejsem úplně jistý, že to takto jde - snad věta o ekvivalenci??)
|- ¬B→¬¬(∀x)¬A
To lze bez újmy na čemkoliv přepsat jako
|- ¬B→¬(∃x)A
A poslední krok je použití A3 a modus ponens
¬B->¬(∃x)A ( ¬B->¬(∃x)A )->( (∃x)A->B ) ---------------------------------------------- (∃x)A->B
|- (∃x)A→B