Type  Label  Description 
Statement 

Theorem  simp1r3 1001 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2l1 1002 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2l2 1003 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2l3 1004 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2r1 1005 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2r2 1006 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2r3 1007 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3l1 1008 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3l2 1009 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3l3 1010 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3r1 1011 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3r2 1012 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3r3 1013 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp11l 1014 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp11r 1015 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp12l 1016 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp12r 1017 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp13l 1018 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp13r 1019 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp21l 1020 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp21r 1021 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp22l 1022 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp22r 1023 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp23l 1024 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp23r 1025 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp31l 1026 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp31r 1027 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp32l 1028 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp32r 1029 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp33l 1030 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp33r 1031 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp111 1032 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp112 1033 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp113 1034 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp121 1035 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp122 1036 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp123 1037 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp131 1038 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp132 1039 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp133 1040 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp211 1041 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp212 1042 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp213 1043 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp221 1044 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp222 1045 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp223 1046 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp231 1047 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp232 1048 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp233 1049 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp311 1050 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp312 1051 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp313 1052 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp321 1053 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp322 1054 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp323 1055 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp331 1056 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp332 1057 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp333 1058 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  3adantl1 1059 
Deduction adding a conjunct to antecedent. (Contributed by NM,
24Feb2005.)



Theorem  3adantl2 1060 
Deduction adding a conjunct to antecedent. (Contributed by NM,
24Feb2005.)



Theorem  3adantl3 1061 
Deduction adding a conjunct to antecedent. (Contributed by NM,
24Feb2005.)



Theorem  3adantr1 1062 
Deduction adding a conjunct to antecedent. (Contributed by NM,
27Apr2005.)



Theorem  3adantr2 1063 
Deduction adding a conjunct to antecedent. (Contributed by NM,
27Apr2005.)



Theorem  3adantr3 1064 
Deduction adding a conjunct to antecedent. (Contributed by NM,
27Apr2005.)



Theorem  3ad2antl1 1065 
Deduction adding conjuncts to antecedent. (Contributed by NM,
4Aug2007.)



Theorem  3ad2antl2 1066 
Deduction adding conjuncts to antecedent. (Contributed by NM,
4Aug2007.)



Theorem  3ad2antl3 1067 
Deduction adding conjuncts to antecedent. (Contributed by NM,
4Aug2007.)



Theorem  3ad2antr1 1068 
Deduction adding a conjuncts to antecedent. (Contributed by NM,
25Dec2007.)



Theorem  3ad2antr2 1069 
Deduction adding a conjuncts to antecedent. (Contributed by NM,
27Dec2007.)



Theorem  3ad2antr3 1070 
Deduction adding a conjuncts to antecedent. (Contributed by NM,
30Dec2007.)



Theorem  3anibar 1071 
Remove a hypothesis from the second member of a biimplication.
(Contributed by FL, 22Jul2008.)



Theorem  3mix1 1072 
Introduction in triple disjunction. (Contributed by NM, 4Apr1995.)



Theorem  3mix2 1073 
Introduction in triple disjunction. (Contributed by NM, 4Apr1995.)



Theorem  3mix3 1074 
Introduction in triple disjunction. (Contributed by NM, 4Apr1995.)



Theorem  3mix1i 1075 
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6Oct2014.)



Theorem  3mix2i 1076 
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6Oct2014.)



Theorem  3mix3i 1077 
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6Oct2014.)



Theorem  3mix1d 1078 
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8Jun2011.)



Theorem  3mix2d 1079 
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8Jun2011.)



Theorem  3mix3d 1080 
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8Jun2011.)



Theorem  3pm3.2i 1081 
Infer conjunction of premises. (Contributed by NM, 10Feb1995.)



Theorem  pm3.2an3 1082 
pm3.2 126 for a triple conjunction. (Contributed by
Alan Sare,
24Oct2011.)



Theorem  3jca 1083 
Join consequents with conjunction. (Contributed by NM, 9Apr1994.)



Theorem  3jcad 1084 
Deduction conjoining the consequents of three implications.
(Contributed by NM, 25Sep2005.)



Theorem  mpbir3an 1085 
Detach a conjunction of truths in a biconditional. (Contributed by NM,
16Sep2011.) (Revised by NM, 9Jan2015.)



Theorem  mpbir3and 1086 
Detach a conjunction of truths in a biconditional. (Contributed by
Mario Carneiro, 11May2014.)



Theorem  syl3anbrc 1087 
Syllogism inference. (Contributed by Mario Carneiro, 11May2014.)



Theorem  3anim123i 1088 
Join antecedents and consequents with conjunction. (Contributed by NM,
8Apr1994.)



Theorem  3anim1i 1089 
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16Aug2009.)



Theorem  3anim2i 1090 
Add two conjuncts to antecedent and consequent. (Contributed by AV,
21Nov2019.)



Theorem  3anim3i 1091 
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 19Aug2009.)



Theorem  3anbi123i 1092 
Join 3 biconditionals with conjunction. (Contributed by NM,
21Apr1994.)



Theorem  3orbi123i 1093 
Join 3 biconditionals with disjunction. (Contributed by NM,
17May1994.)



Theorem  3anbi1i 1094 
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8Sep2006.)



Theorem  3anbi2i 1095 
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8Sep2006.)



Theorem  3anbi3i 1096 
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8Sep2006.)



Theorem  3imp 1097 
Importation inference. (Contributed by NM, 8Apr1994.)



Theorem  3impa 1098 
Importation from double to triple conjunction. (Contributed by NM,
20Aug1995.)



Theorem  3impb 1099 
Importation from double to triple conjunction. (Contributed by NM,
20Aug1995.)



Theorem  3impia 1100 
Importation to triple conjunction. (Contributed by NM, 13Jun2006.)

