HomeHome Intuitionistic Logic Explorer
Theorem List (p. 11 of 20)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1001-1100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsimpl23 1001 Simplification of conjunction.
 
Theoremsimpl31 1002 Simplification of conjunction.
 
Theoremsimpl32 1003 Simplification of conjunction.
 
Theoremsimpl33 1004 Simplification of conjunction.
 
Theoremsimpr11 1005 Simplification of conjunction.
 
Theoremsimpr12 1006 Simplification of conjunction.
 
Theoremsimpr13 1007 Simplification of conjunction.
 
Theoremsimpr21 1008 Simplification of conjunction.
 
Theoremsimpr22 1009 Simplification of conjunction.
 
Theoremsimpr23 1010 Simplification of conjunction.
 
Theoremsimpr31 1011 Simplification of conjunction.
 
Theoremsimpr32 1012 Simplification of conjunction.
 
Theoremsimpr33 1013 Simplification of conjunction.
 
Theoremsimp1l1 1014 Simplification of conjunction.
 
Theoremsimp1l2 1015 Simplification of conjunction.
 
Theoremsimp1l3 1016 Simplification of conjunction.
 
Theoremsimp1r1 1017 Simplification of conjunction.
 
Theoremsimp1r2 1018 Simplification of conjunction.
 
Theoremsimp1r3 1019 Simplification of conjunction.
 
Theoremsimp2l1 1020 Simplification of conjunction.
 
Theoremsimp2l2 1021 Simplification of conjunction.
 
Theoremsimp2l3 1022 Simplification of conjunction.
 
Theoremsimp2r1 1023 Simplification of conjunction.
 
Theoremsimp2r2 1024 Simplification of conjunction.
 
Theoremsimp2r3 1025 Simplification of conjunction.
 
Theoremsimp3l1 1026 Simplification of conjunction.
 
Theoremsimp3l2 1027 Simplification of conjunction.
 
Theoremsimp3l3 1028 Simplification of conjunction.
 
Theoremsimp3r1 1029 Simplification of conjunction.
 
Theoremsimp3r2 1030 Simplification of conjunction.
 
Theoremsimp3r3 1031 Simplification of conjunction.
 
Theoremsimp11l 1032 Simplification of conjunction.
 
Theoremsimp11r 1033 Simplification of conjunction.
 
Theoremsimp12l 1034 Simplification of conjunction.
 
Theoremsimp12r 1035 Simplification of conjunction.
 
Theoremsimp13l 1036 Simplification of conjunction.
 
Theoremsimp13r 1037 Simplification of conjunction.
 
Theoremsimp21l 1038 Simplification of conjunction.
 
Theoremsimp21r 1039 Simplification of conjunction.
 
Theoremsimp22l 1040 Simplification of conjunction.
 
Theoremsimp22r 1041 Simplification of conjunction.
 
Theoremsimp23l 1042 Simplification of conjunction.
 
Theoremsimp23r 1043 Simplification of conjunction.
 
Theoremsimp31l 1044 Simplification of conjunction.
 
Theoremsimp31r 1045 Simplification of conjunction.
 
Theoremsimp32l 1046 Simplification of conjunction.
 
Theoremsimp32r 1047 Simplification of conjunction.
 
Theoremsimp33l 1048 Simplification of conjunction.
 
Theoremsimp33r 1049 Simplification of conjunction.
 
Theoremsimp111 1050 Simplification of conjunction.
 
Theoremsimp112 1051 Simplification of conjunction.
 
Theoremsimp113 1052 Simplification of conjunction.
 
Theoremsimp121 1053 Simplification of conjunction.
 
Theoremsimp122 1054 Simplification of conjunction.
 
Theoremsimp123 1055 Simplification of conjunction.
 
Theoremsimp131 1056 Simplification of conjunction.
 
Theoremsimp132 1057 Simplification of conjunction.
 
Theoremsimp133 1058 Simplification of conjunction.
 
Theoremsimp211 1059 Simplification of conjunction.
 
Theoremsimp212 1060 Simplification of conjunction.
 
Theoremsimp213 1061 Simplification of conjunction.
 
Theoremsimp221 1062 Simplification of conjunction.
 
Theoremsimp222 1063 Simplification of conjunction.
 
Theoremsimp223 1064 Simplification of conjunction.
 
Theoremsimp231 1065 Simplification of conjunction.
 
Theoremsimp232 1066 Simplification of conjunction.
 
Theoremsimp233 1067 Simplification of conjunction.
 
Theoremsimp311 1068 Simplification of conjunction.
 
Theoremsimp312 1069 Simplification of conjunction.
 
Theoremsimp313 1070 Simplification of conjunction.
 
Theoremsimp321 1071 Simplification of conjunction.
 
Theoremsimp322 1072 Simplification of conjunction.
 
Theoremsimp323 1073 Simplification of conjunction.
 
Theoremsimp331 1074 Simplification of conjunction.
 
Theoremsimp332 1075 Simplification of conjunction.
 
Theoremsimp333 1076 Simplification of conjunction.
 
Theorem3adantl1 1077 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adantl2 1078 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adantl3 1079 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adantr1 1080 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adantr2 1081 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3adantr3 1082 Deduction adding a conjunct to antecedent.
   =>   
 
Theorem3ad2antl1 1083 Deduction adding conjuncts to antecedent.
   =>   
 
Theorem3ad2antl2 1084 Deduction adding conjuncts to antecedent.
   =>   
 
Theorem3ad2antl3 1085 Deduction adding conjuncts to antecedent.
   =>   
 
Theorem3ad2antr1 1086 Deduction adding a conjuncts to antecedent.
   =>   
 
Theorem3ad2antr2 1087 Deduction adding a conjuncts to antecedent.
   =>   
 
Theorem3ad2antr3 1088 Deduction adding a conjuncts to antecedent.
   =>   
 
Theorem3anibar 1089 Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.)
   =>   
 
Theorem3mix1 1090 Introduction in triple disjunction.
 
Theorem3mix2 1091 Introduction in triple disjunction.
 
Theorem3mix3 1092 Introduction in triple disjunction.
 
Theorem3pm3.2i 1093 Infer conjunction of premises.
   &       &       =>   
 
Theorempm3.2an3 1094 pm3.2 125 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.)
 
Theorem3jca 1095 Join consequents with conjunction.
   &       &       =>   
 
Theorem3jcad 1096 Deduction conjoining the consequents of three implications.
   &       &       =>   
 
Theoremmpbir3an 1097 Detach a conjunction of truths in a biconditional.
   &       &       &       =>   
 
Theoremmpbir3and 1098 Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)
   &       &       &       =>   
 
Theoremmpbir3anOLD 1099 Obsolete version of mpbir3an 1097 as of 9-Jan-2015.
   &       &       &       =>   
 
Theoremmpbir3andOLD 1100 Obsolete version of mpbir3and 1098 as of 9-Jan-2015.
   &       &       &       =>   
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-1914
  Copyright terms: Public domain < Previous  Next >