Can we validate proof by contradiction inside first order (or propositional) logic as formal theory? Am I right that we can use meta theorem of deduction for it ($ \phi \vdash (\psi \land \neg \psi) \Rightarrow \vdash \phi \rightarrow (\psi \land \neg \psi) \Rightarrow$ ..contraposition derivation.. $ (\psi \lor \neg \psi) \rightarrow \neg \phi. MP \neg \phi $ ).
Thanks.