ex1 matita

theorem ex1 : (A ⇒ C) ⇒ (B ⇒ C) ⇒ A ∨ B ⇒ C.
apply rule (prove ((A ⇒ C) ⇒ (B ⇒ C) ⇒ A ∨ B ⇒ C));
apply rule (⇒#i [H1] ((B⇒ C) ⇒ A ∨ B ⇒ C));
apply rule (⇒#i [H2] (A ∨ B ⇒ C));
apply rule (⇒#i [H3] (C));
apply rule (∨#e (A ∨ B) [H01] (C) [H02] (C));
	[apply rule (discharge [H3]);
	|apply rule (⇒#e (A ⇒ C) (A));
	  [apply rule (discharge [H1]);
	  |apply rule (discharge [H01]);
	  ]
	|apply rule (⇒#e (B ⇒ C) (B));
	  [apply rule (discharge [H2]);
	  |apply rule (discharge [H02]);
	  ]
	]

qed.