The abstract of the Mizar article:

Calculus of Propositions

by

Jan Popiolek, and

Andrzej Trybulec

Received October 23, 1990

MML identifier: PROCAL_1

[ Mizar article, MML identifier index ]

environ

 vocabulary CQC_LANG, ZF_LANG, CQC_THE1;
 notation SUBSET_1, CQC_LANG, CQC_THE1;
 constructors CQC_THE1, XBOOLE_0;
 clusters CQC_LANG, ZFMISC_1, XBOOLE_0;


begin
 reserve p, q, r, s for Element of CQC-WFF;

             :::::::::::::::::::::::::::::
             ::   T A U T O L O G I E   ::
             :::::::::::::::::::::::::::::

theorem :: PROCAL_1:1
  'not' ( p '&' 'not' p ) in TAUT;

theorem :: PROCAL_1:2
  p 'or' 'not' p in TAUT;

theorem :: PROCAL_1:3
  p => ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:4
  q => ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:5
  ( p 'or' q ) => ( 'not' p => q ) in TAUT;

theorem :: PROCAL_1:6
  'not' ( p 'or' q ) => ( 'not' p '&' 'not' q ) in TAUT;

theorem :: PROCAL_1:7
  ( 'not' p '&' 'not' q ) => 'not' ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:8
  ( p 'or' q ) => ( q 'or' p ) in TAUT;

theorem :: PROCAL_1:9
    'not' p 'or' p in TAUT;

theorem :: PROCAL_1:10
    'not' ( p 'or' q ) => 'not' p in TAUT;

theorem :: PROCAL_1:11
  ( p 'or' p ) => p in TAUT;

theorem :: PROCAL_1:12
    p => ( p 'or' p ) in TAUT;

theorem :: PROCAL_1:13
    ( p '&' 'not' p ) => q in TAUT;

theorem :: PROCAL_1:14
    ( p => q ) => ( 'not' p 'or' q ) in TAUT;

theorem :: PROCAL_1:15
  ( p '&' q ) => 'not' ( p => 'not' q ) in TAUT;

theorem :: PROCAL_1:16
  'not' ( p => 'not' q ) => ( p '&' q ) in TAUT;

theorem :: PROCAL_1:17
  'not' ( p '&' q ) => ( 'not' p 'or' 'not' q ) in TAUT;

theorem :: PROCAL_1:18
  ( 'not' p 'or' 'not' q ) => 'not' ( p '&' q ) in TAUT;

theorem :: PROCAL_1:19
  ( p '&' q ) => p in TAUT;

theorem :: PROCAL_1:20
  ( p '&' q ) => ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:21
  ( p '&' q ) => q in TAUT;

theorem :: PROCAL_1:22
    p => p '&' p in TAUT;

theorem :: PROCAL_1:23
    ( p <=> q ) => ( p => q ) in TAUT;

theorem :: PROCAL_1:24
    ( p <=> q ) => ( q => p ) in TAUT;

theorem :: PROCAL_1:25
  (( p 'or' q ) 'or' r ) => ( p 'or' ( q 'or' r )) in TAUT;

theorem :: PROCAL_1:26
    (( p '&' q ) '&' r ) => ( p '&' ( q '&' r )) in TAUT;

theorem :: PROCAL_1:27
  ( p 'or' ( q 'or' r )) => (( p 'or' q ) 'or' r ) in TAUT;

theorem :: PROCAL_1:28
  p => ( q => ( p '&' q )) in TAUT;

theorem :: PROCAL_1:29
    ( p => q ) => (( q => p ) => ( p <=> q )) in TAUT;

theorem :: PROCAL_1:30
    ( p 'or' q ) <=> ( q 'or' p ) in TAUT;

theorem :: PROCAL_1:31
    (( p '&' q ) => r ) => ( p => ( q => r )) in TAUT;

theorem :: PROCAL_1:32
  ( p => ( q => r )) => (( p '&' q ) => r ) in TAUT;

theorem :: PROCAL_1:33
  ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in TAUT;

theorem :: PROCAL_1:34
    (( p 'or' q ) => r ) => (( p => r ) 'or' ( q => r )) in TAUT;

theorem :: PROCAL_1:35
  ( p => r ) => (( q => r ) => (( p 'or' q ) => r)) in TAUT;

theorem :: PROCAL_1:36
  (( p => r ) '&' ( q => r )) => (( p 'or' q ) => r) in TAUT;

theorem :: PROCAL_1:37
    ( p => ( q '&' 'not' q )) => 'not' p in TAUT;

theorem :: PROCAL_1:38
    (( p 'or' q ) '&' ( p 'or' r )) => ( p 'or' ( q '&' r )) in TAUT;

theorem :: PROCAL_1:39
    ( p '&' ( q 'or' r )) => (( p '&' q ) 'or' ( p '&' r )) in TAUT;

theorem :: PROCAL_1:40
  (( p 'or' r ) '&' ( q 'or' r )) => (( p '&' q ) 'or' r ) in TAUT;

theorem :: PROCAL_1:41
    (( p 'or' q ) '&' r ) => (( p '&' r ) 'or' ( q '&' r )) in TAUT;

          ::::::::::::::::::::::::::::::::::::::::::::
          ::   R E G U L Y   D O W O D Z E N I A    ::
          ::::::::::::::::::::::::::::::::::::::::::::

theorem :: PROCAL_1:42
    p in TAUT implies ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:43
    q in TAUT implies ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:44
    ( p '&' q ) in TAUT implies p in TAUT;

theorem :: PROCAL_1:45
    ( p '&' q ) in TAUT implies q in TAUT;

theorem :: PROCAL_1:46
    ( p '&' q ) in TAUT implies ( p 'or' q ) in TAUT;

theorem :: PROCAL_1:47
   p in TAUT & q in TAUT implies p '&' q in TAUT;

theorem :: PROCAL_1:48
   p => q in TAUT implies ( p 'or' r ) => ( q 'or' r ) in TAUT;

theorem :: PROCAL_1:49
   p => q in TAUT implies ( r 'or' p ) => ( r 'or' q ) in TAUT;

theorem :: PROCAL_1:50
   p => q in TAUT implies ( r '&' p ) => ( r '&' q ) in TAUT;

theorem :: PROCAL_1:51
  p => q in TAUT implies ( p '&' r ) => ( q '&' r ) in TAUT;

theorem :: PROCAL_1:52
    r => p in TAUT & r => q in TAUT implies r => ( p '&' q ) in TAUT;

theorem :: PROCAL_1:53
    p => r in TAUT & q => r in TAUT implies ( p 'or' q ) => r in TAUT;

theorem :: PROCAL_1:54
    ( p 'or' q ) in TAUT & 'not' p in TAUT implies q in TAUT;

theorem :: PROCAL_1:55
    ( p 'or' q ) in TAUT & 'not' q in TAUT implies p in TAUT;

theorem :: PROCAL_1:56
    p => q in TAUT & r => s in TAUT implies ( p '&' r ) => ( q '&' s ) in TAUT;

theorem :: PROCAL_1:57
    p => q in TAUT & r => s in TAUT implies ( p 'or' r ) => ( q 'or' s ) in
TAUT;

theorem :: PROCAL_1:58
    ( p '&' 'not' q ) => 'not' p in TAUT implies p => q in TAUT;