# Predicate logic

THEOREM    $$\exists x : P(x) \vdash \neg \forall x : \neg P(x)$$

Proof available

THEOREM    $$\forall x : P(x) \vdash \neg \exists x : \neg P(x)$$

Proof available

THEOREM    $$\exists x,y : P(x, y) \vdash \exists y,x : P(x, y)$$

Proof available

THEOREM    $$\forall x,y : P(x, y) \vdash \forall y,x : P(x, y)$$

Proof available

THEOREM    $$\forall x : P(x) \wedge Q(x) \vdash [\forall x : P(x)] \wedge [\forall x : Q(x)]$$

Proof available

THEOREM    $$[\forall x : P(x)] \wedge [\forall x : Q(x)] \vdash \forall x : P(x) \wedge Q(x)$$

Proof available

THEOREM    $$\forall x : P(x) \wedge Q(x) \dashv\vdash [\forall x : P(x)] \wedge [\forall x : Q(x)]$$

Proof unavailable

THEOREM    $$\exists x : P(x) \vee Q(x) \vdash [\exists x : P(x)] \vee [\exists x : Q(x)]$$

Proof available

THEOREM    $$[\exists x : P(x)] \vee [\exists x : Q(x)] \vdash \exists x : P(x) \vee Q(x)$$

Proof available

THEOREM    $$\exists x : P(x) \vee Q(x) \dashv\vdash [\exists x : P(x)] \vee [\exists x : Q(x)]$$

Proof unavailable

THEOREM    $$\forall x : P(x) \Rightarrow Q(x) \vdash [\forall x : P(x)] \Rightarrow [\forall x : Q(x)]$$

Proof available

THEOREM    $$P \Rightarrow Q \Rightarrow R \vdash P \wedge Q \Rightarrow R$$

Proof available

THEOREM    $$P \wedge Q \Rightarrow R \vdash P \Rightarrow Q \Rightarrow R$$

Proof available

THEOREM    $$P \Rightarrow Q \Rightarrow R \dashv\vdash P \wedge Q \Rightarrow R$$

Proof unavailable