:: Consequences of the Sequent Calculus
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004 Association of Mizar Users
:: deftheorem defines seq CALCUL_2:def 1 :
theorem Th1: :: CALCUL_2:1
theorem Th2: :: CALCUL_2:2
theorem Th3: :: CALCUL_2:3
theorem Th4: :: CALCUL_2:4
theorem Th5: :: CALCUL_2:5
theorem Th6: :: CALCUL_2:6
theorem Th7: :: CALCUL_2:7
theorem :: CALCUL_2:8
theorem :: CALCUL_2:9
theorem Th10: :: CALCUL_2:10
theorem Th11: :: CALCUL_2:11
theorem Th12: :: CALCUL_2:12
theorem Th13: :: CALCUL_2:13
theorem Th14: :: CALCUL_2:14
theorem Th15: :: CALCUL_2:15
theorem Th16: :: CALCUL_2:16
theorem Th17: :: CALCUL_2:17
theorem Th18: :: CALCUL_2:18
:: deftheorem defines Per CALCUL_2:def 2 :
theorem Th19: :: CALCUL_2:19
theorem Th20: :: CALCUL_2:20
:: deftheorem Def3 defines Begin CALCUL_2:def 3 :
:: deftheorem Def4 defines Impl CALCUL_2:def 4 :
theorem Th21: :: CALCUL_2:21
theorem Th22: :: CALCUL_2:22
theorem Th23: :: CALCUL_2:23
theorem Th24: :: CALCUL_2:24
theorem Th25: :: CALCUL_2:25
theorem Th26: :: CALCUL_2:26
theorem Th27: :: CALCUL_2:27
theorem Th28: :: CALCUL_2:28
theorem Th29: :: CALCUL_2:29
theorem :: CALCUL_2:30
theorem Th31: :: CALCUL_2:31
theorem :: CALCUL_2:32