Type  Label  Description 
Statement 

Theorem  3simpb 901 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  3simpc 902 
Simplification of triple conjunction. (Contributed by NM, 21Apr1994.)
(Proof shortened by Andrew Salmon, 13May2011.)



Theorem  simp1 903 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  simp2 904 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  simp3 905 
Simplification of triple conjunction. (Contributed by NM,
21Apr1994.)



Theorem  simpl1 906 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpl2 907 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpl3 908 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpr1 909 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpr2 910 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simpr3 911 
Simplification rule. (Contributed by Jeff Hankins, 17Nov2009.)



Theorem  simp1i 912 
Infer a conjunct from a triple conjunction. (Contributed by NM,
19Apr2005.)



Theorem  simp2i 913 
Infer a conjunct from a triple conjunction. (Contributed by NM,
19Apr2005.)



Theorem  simp3i 914 
Infer a conjunct from a triple conjunction. (Contributed by NM,
19Apr2005.)



Theorem  simp1d 915 
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4Sep2005.)



Theorem  simp2d 916 
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4Sep2005.)



Theorem  simp3d 917 
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4Sep2005.)



Theorem  simp1bi 918 
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  simp2bi 919 
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  simp3bi 920 
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  3adant1 921 
Deduction adding a conjunct to antecedent. (Contributed by NM,
16Jul1995.)



Theorem  3adant2 922 
Deduction adding a conjunct to antecedent. (Contributed by NM,
16Jul1995.)



Theorem  3adant3 923 
Deduction adding a conjunct to antecedent. (Contributed by NM,
16Jul1995.)



Theorem  3ad2ant1 924 
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21Apr2005.)



Theorem  3ad2ant2 925 
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21Apr2005.)



Theorem  3ad2ant3 926 
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21Apr2005.)



Theorem  simp1l 927 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp1r 928 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp2l 929 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp2r 930 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp3l 931 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp3r 932 
Simplification of triple conjunction. (Contributed by NM, 9Nov2011.)



Theorem  simp11 933 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp12 934 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp13 935 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp21 936 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp22 937 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp23 938 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp31 939 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp32 940 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simp33 941 
Simplification of doubly triple conjunction. (Contributed by NM,
17Nov2011.)



Theorem  simpll1 942 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpll2 943 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpll3 944 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simplr1 945 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simplr2 946 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simplr3 947 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simprl1 948 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simprl2 949 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simprl3 950 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simprr1 951 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simprr2 952 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simprr3 953 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl1l 954 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl1r 955 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl2l 956 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl2r 957 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl3l 958 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl3r 959 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr1l 960 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr1r 961 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr2l 962 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr2r 963 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr3l 964 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr3r 965 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1ll 966 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1lr 967 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1rl 968 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1rr 969 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2ll 970 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2lr 971 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2rl 972 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp2rr 973 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3ll 974 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3lr 975 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3rl 976 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp3rr 977 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl11 978 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl12 979 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl13 980 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl21 981 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl22 982 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl23 983 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl31 984 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl32 985 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpl33 986 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr11 987 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr12 988 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr13 989 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr21 990 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr22 991 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr23 992 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr31 993 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr32 994 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simpr33 995 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1l1 996 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1l2 997 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1l3 998 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1r1 999 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp1r2 1000 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)

