Let and Then implies . Proof Let be a proof of from Let be a model of . Need We prove by induction on If is a premiss then since is a model of If is an axiom then (all axioms are tautologies) If follows by MP, then by induction check