HomeHome Intuitionistic Logic Explorer
Theorem List (p. 11 of 22)
< 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
 
Theoremsimp223 1001 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp231 1002 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp232 1003 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp233 1004 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp311 1005 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp312 1006 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp313 1007 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp321 1008 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp322 1009 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp323 1010 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp331 1011 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp332 1012 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimp333 1013 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theorem3adantl1 1014 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
   =>   
 
Theorem3adantl2 1015 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
   =>   
 
Theorem3adantl3 1016 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
   =>   
 
Theorem3adantr1 1017 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
   =>   
 
Theorem3adantr2 1018 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
   =>   
 
Theorem3adantr3 1019 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
   =>   
 
Theorem3ad2antl1 1020 Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
   =>   
 
Theorem3ad2antl2 1021 Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
   =>   
 
Theorem3ad2antl3 1022 Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
   =>   
 
Theorem3ad2antr1 1023 Deduction adding a conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
   =>   
 
Theorem3ad2antr2 1024 Deduction adding a conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
   =>   
 
Theorem3ad2antr3 1025 Deduction adding a conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)
   =>   
 
Theorem3anibar 1026 Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.)
   =>   
 
Theorem3mix1 1027 Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
 
Theorem3mix2 1028 Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
 
Theorem3mix3 1029 Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
 
Theorem3pm3.2i 1030 Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
   &       &       =>   
 
Theorempm3.2an3 1031 pm3.2 124 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.)
 
Theorem3jca 1032 Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
   &       &       =>   
 
Theorem3jcad 1033 Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
   &       &       =>   
 
Theoremmpbir3an 1034 Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
   &       &       &       =>   
 
Theoremmpbir3and 1035 Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)
   &       &       &       =>   
 
Theoremmpbir3anOLD 1036 Obsolete version of mpbir3an 1034 as of 9-Jan-2015. (Contributed by NM, 16-Sep-2011.)
   &       &       &       =>   
 
Theoremmpbir3andOLD 1037 Obsolete version of mpbir3and 1035 as of 9-Jan-2015. (Contributed by NM, 11-May-2014.)
   &       &       &       =>   
 
Theoremsyl3anbrc 1038 Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
   &       &       &       =>   
 
Theorem3anim123i 1039 Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
   &       &       =>   
 
Theorem3anim1i 1040 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
   =>   
 
Theorem3anim3i 1041 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
   =>   
 
Theorem3anbi123i 1042 Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
   &       &       =>   
 
Theorem3orbi123i 1043 Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
   &       &       =>   
 
Theorem3anbi1i 1044 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
   =>   
 
Theorem3anbi2i 1045 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
   =>   
 
Theorem3anbi3i 1046 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
   =>   
 
Theorem3imp 1047 Importation inference. (Contributed by NM, 8-Apr-1994.)
   =>   
 
Theorem3impa 1048 Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
   =>   
 
Theorem3impb 1049 Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
   =>   
 
Theorem3impia 1050 Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
   =>   
 
Theorem3impib 1051 Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
   =>   
 
Theorem3exp 1052 Exportation inference. (Contributed by NM, 30-May-1994.)
   =>   
 
Theorem3expa 1053 Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
   =>   
 
Theorem3expb 1054 Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
   =>   
 
Theorem3expia 1055 Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
   =>   
 
Theorem3expib 1056 Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
   =>   
 
Theorem3com12 1057 Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
   =>   
 
Theorem3com13 1058 Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
   =>   
 
Theorem3com23 1059 Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
   =>   
 
Theorem3coml 1060 Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
   =>   
 
Theorem3comr 1061 Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
   =>   
 
Theorem3adant3r1 1062 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
   =>   
 
Theorem3adant3r2 1063 Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
   =>   
 
Theorem3adant3r3 1064 Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
   =>   
 
Theorem3an1rs 1065 Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
   =>   
 
Theorem3imp1 1066 Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
   =>   
 
Theorem3impd 1067 Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
   =>   
 
Theorem3imp2 1068 Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
   =>   
 
Theorem3exp1 1069 Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
   =>   
 
Theorem3expd 1070 Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
   =>   
 
Theorem3exp2 1071 Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
   =>   
 
Theoremexp5o 1072 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
   =>   
 
Theoremexp516 1073 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
   =>   
 
Theoremexp520 1074 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
   =>   
 
Theorem3adant1l 1075 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
   =>   
 
Theorem3adant1r 1076 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
   =>   
 
Theorem3adant2l 1077 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
   =>   
 
Theorem3adant2r 1078 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
   =>   
 
Theorem3adant3l 1079 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
   =>   
 
Theorem3adant3r 1080 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
   =>   
 
Theoremsyl12anc 1081 Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
   &       &       &       =>   
 
Theoremsyl21anc 1082 Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
   &       &       &       =>   
 
Theoremsyl3anc 1083 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       =>   
 
Theoremsyl22anc 1084 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       =>   
 
Theoremsyl13anc 1085 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       =>   
 
Theoremsyl31anc 1086 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       =>   
 
Theoremsyl112anc 1087 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       =>   
 
Theoremsyl121anc 1088 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       =>   
 
Theoremsyl211anc 1089 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       =>   
 
Theoremsyl23anc 1090 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl32anc 1091 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl122anc 1092 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl212anc 1093 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl221anc 1094 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl113anc 1095 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl131anc 1096 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl311anc 1097 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       =>   
 
Theoremsyl33anc 1098 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       =>   
 
Theoremsyl222anc 1099 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       =>   
 
Theoremsyl123anc 1100 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
   &       &       &       &       &       &       =>   
    < 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-2000 21 2001-2100 22 2101-2186
  Copyright terms: Public domain < Previous  Next >