% prop0.tut

proof mp: A & (A=>B) => B = 
begin
[A & (A=>B);		% 1 Assumption
 A=>B;			% 2 AndE2 1
 A;			% 3 AndE1 2 
 B ];			% 4 ImpE 2 3
A & (A=>B) => B         % 5 ImpI 4
end;

% prop3.tut
% Classical implication definition  ~A|B => A=>B

proof ImpDef : ~A|B => A=>B =
begin
[~A|B;
  [A;
    [~A;
      F;	
      B];
    [B;	
     B];
   B;
  ];
  A => B];
~A|B => A=>B	
end;