[PL11] Derivation rules

∀E (Universal Quantifier Elimination)
For any variable v and name c, if you have derived ∀vφ, then you can write down φv/c, depending on everything ∀vφ depends on.

∃I (Existential Quantifier Introduction)
For any variable v and name c, if you have derived φv/c, and ∃vφ is a well-formed formula of MPL, then you can write down ∃vφ, depending on everything φv/c depends on.

∀I (Universal Quantifier Introduction)
For any variable v and name c, if you have derived φv/c, and c does not occur in φ, and c does not occur in anything φv/c depends on, and ∀vφ is a well-formed formula of MPL, then you can write down ∀vφ, depending on everything φv/c depends on.

∃E (Existential Quantifier Elimination)
For any variable v and name c, if you have derived ∃vφ, assumed φv/c, and derived ψ, and c does not occur in ψ, φ, or anything ψ depends on (except φv/c), then you can write down ψ a second time, depending on everything the first ψ depends on (except the assumption φv/c) together with everything ∃vφ depends on.

A (Rule of Assumption)
You can write down any MPL wff, depending on itself.

&I (Conjunction Introduction)
If you have derived φ and ψ, you can write down (φ&ψ), depending on everything φ and ψ depend on.

&E (Conjunction Elimination)
If you have derived (φ&ψ), you can write down φ or ψ, depending on everything (φ&ψ) depends on.

→I (Conditional Introduction)
If you have assumed φ, and you have derived ψ, you can write down (φ→ψ), depending on everything ψ depends on except φ.

→E (Conditional Elimination or Modus Ponens)
If you have derived (φ→ψ) and φ, you can write down ψ, depending on everything (φ→ψ) and φ depend on.

~I (Negation Introduction)
If you have assumed ψ, and you have derived (φ&~φ), then you can write down ~ψ, depending on everything (φ&~φ) depends on except ψ.

~E (Negation Elimination)
If you have assumed ~ψ, and you have derived (φ&~φ), then you can write down ψ, depending on everything (φ&~φ) depends on except ~ψ.

∨I (Disjunction Introduction)
If you have derived φ, you can write down (φ∨ψ) or (ψ∨φ), depending on everything φ depends on. (ψ is any MPL wff.)

∨E (Disjunction Elimination or Disjunctive Syllogism)
If you have derived (φ∨ψ) and ~ψ, you can write down φ, depending on everything (φ∨ψ) and ~ψ depend on.

Also, if you have derived (φ∨ψ) and ~φ, you can write down ψ, depending on everything (φ∨ψ) and ~φ depend on.

PC (Proof by Cases)
If you have derived (φ∨ψ) and (φ→α) and (ψ→β), then you can write down (α∨β), depending on everything (φ∨ψ) and (φ→α) and (ψ→β) depend on.

↔I (Biconditional Introduction)
If you have derived ((φ→ψ)&(ψ→φ)), you can write down (φ↔ψ), depending on everything ((φ→ψ)&(ψ→φ)) depends on.

↔E (Biconditional Elimination)
If you have derived (φ↔ψ), you can write down ((φ→ψ)&(ψ→φ)) depending on everything (φ↔ψ) depends on.