P. 11 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 1001-1100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	simprl2 1001	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ ∧ χ) ∧ θ)) → ψ)
Theorem	simprl3 1002	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ ∧ χ) ∧ θ)) → χ)
Theorem	simprr1 1003	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (θ ∧ (φ ∧ ψ ∧ χ))) → φ)
Theorem	simprr2 1004	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (θ ∧ (φ ∧ ψ ∧ χ))) → ψ)
Theorem	simprr3 1005	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (θ ∧ (φ ∧ ψ ∧ χ))) → χ)
Theorem	simpl1l 1006	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ) ∧ χ ∧ θ) ∧ τ) → φ)
Theorem	simpl1r 1007	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ) ∧ χ ∧ θ) ∧ τ) → ψ)
Theorem	simpl2l 1008	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ (φ ∧ ψ) ∧ θ) ∧ τ) → φ)
Theorem	simpl2r 1009	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ (φ ∧ ψ) ∧ θ) ∧ τ) → ψ)
Theorem	simpl3l 1010	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ θ ∧ (φ ∧ ψ)) ∧ τ) → φ)
Theorem	simpl3r 1011	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ θ ∧ (φ ∧ ψ)) ∧ τ) → ψ)
Theorem	simpr1l 1012	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ) ∧ χ ∧ θ)) → φ)
Theorem	simpr1r 1013	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ) ∧ χ ∧ θ)) → ψ)
Theorem	simpr2l 1014	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ (φ ∧ ψ) ∧ θ)) → φ)
Theorem	simpr2r 1015	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ (φ ∧ ψ) ∧ θ)) → ψ)
Theorem	simpr3l 1016	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ θ ∧ (φ ∧ ψ))) → φ)
Theorem	simpr3r 1017	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ θ ∧ (φ ∧ ψ))) → ψ)
Theorem	simp1ll 1018	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ) ∧ χ) ∧ θ ∧ τ) → φ)
Theorem	simp1lr 1019	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ) ∧ χ) ∧ θ ∧ τ) → ψ)
Theorem	simp1rl 1020	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ (φ ∧ ψ)) ∧ θ ∧ τ) → φ)
Theorem	simp1rr 1021	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ (φ ∧ ψ)) ∧ θ ∧ τ) → ψ)
Theorem	simp2ll 1022	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ ((φ ∧ ψ) ∧ χ) ∧ τ) → φ)
Theorem	simp2lr 1023	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ ((φ ∧ ψ) ∧ χ) ∧ τ) → ψ)
Theorem	simp2rl 1024	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ (χ ∧ (φ ∧ ψ)) ∧ τ) → φ)
Theorem	simp2rr 1025	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ (χ ∧ (φ ∧ ψ)) ∧ τ) → ψ)
Theorem	simp3ll 1026	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ τ ∧ ((φ ∧ ψ) ∧ χ)) → φ)
Theorem	simp3lr 1027	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ τ ∧ ((φ ∧ ψ) ∧ χ)) → ψ)
Theorem	simp3rl 1028	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ τ ∧ (χ ∧ (φ ∧ ψ))) → φ)
Theorem	simp3rr 1029	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((θ ∧ τ ∧ (χ ∧ (φ ∧ ψ))) → ψ)
Theorem	simpl11 1030	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ η) → φ)
Theorem	simpl12 1031	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ η) → ψ)
Theorem	simpl13 1032	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ η) → χ)
Theorem	simpl21 1033	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ η) → φ)
Theorem	simpl22 1034	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ η) → ψ)
Theorem	simpl23 1035	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ η) → χ)
Theorem	simpl31 1036	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ η) → φ)
Theorem	simpl32 1037	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ η) → ψ)
Theorem	simpl33 1038	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ η) → χ)
Theorem	simpr11 1039	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ)) → φ)
Theorem	simpr12 1040	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ)) → ψ)
Theorem	simpr13 1041	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ)) → χ)
Theorem	simpr21 1042	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ)) → φ)
Theorem	simpr22 1043	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ)) → ψ)
Theorem	simpr23 1044	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ)) → χ)
Theorem	simpr31 1045	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ))) → φ)
Theorem	simpr32 1046	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ))) → ψ)
Theorem	simpr33 1047	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ))) → χ)
Theorem	simp1l1 1048	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ) ∧ τ ∧ η) → φ)
Theorem	simp1l2 1049	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ) ∧ τ ∧ η) → ψ)
Theorem	simp1l3 1050	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ) ∧ τ ∧ η) → χ)
Theorem	simp1r1 1051	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ)) ∧ τ ∧ η) → φ)
Theorem	simp1r2 1052	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ)) ∧ τ ∧ η) → ψ)
Theorem	simp1r3 1053	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ)) ∧ τ ∧ η) → χ)
Theorem	simp2l1 1054	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ ∧ χ) ∧ θ) ∧ η) → φ)
Theorem	simp2l2 1055	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ ∧ χ) ∧ θ) ∧ η) → ψ)
Theorem	simp2l3 1056	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ ∧ χ) ∧ θ) ∧ η) → χ)
Theorem	simp2r1 1057	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (θ ∧ (φ ∧ ψ ∧ χ)) ∧ η) → φ)
Theorem	simp2r2 1058	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (θ ∧ (φ ∧ ψ ∧ χ)) ∧ η) → ψ)
Theorem	simp2r3 1059	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (θ ∧ (φ ∧ ψ ∧ χ)) ∧ η) → χ)
Theorem	simp3l1 1060	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ ((φ ∧ ψ ∧ χ) ∧ θ)) → φ)
Theorem	simp3l2 1061	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ ((φ ∧ ψ ∧ χ) ∧ θ)) → ψ)
Theorem	simp3l3 1062	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ ((φ ∧ ψ ∧ χ) ∧ θ)) → χ)
Theorem	simp3r1 1063	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ (θ ∧ (φ ∧ ψ ∧ χ))) → φ)
Theorem	simp3r2 1064	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ (θ ∧ (φ ∧ ψ ∧ χ))) → ψ)
Theorem	simp3r3 1065	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ (θ ∧ (φ ∧ ψ ∧ χ))) → χ)
Theorem	simp11l 1066	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ) ∧ χ ∧ θ) ∧ τ ∧ η) → φ)
Theorem	simp11r 1067	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ) ∧ χ ∧ θ) ∧ τ ∧ η) → ψ)
Theorem	simp12l 1068	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ (φ ∧ ψ) ∧ θ) ∧ τ ∧ η) → φ)
Theorem	simp12r 1069	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ (φ ∧ ψ) ∧ θ) ∧ τ ∧ η) → ψ)
Theorem	simp13l 1070	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ θ ∧ (φ ∧ ψ)) ∧ τ ∧ η) → φ)
Theorem	simp13r 1071	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((χ ∧ θ ∧ (φ ∧ ψ)) ∧ τ ∧ η) → ψ)
Theorem	simp21l 1072	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ) ∧ χ ∧ θ) ∧ η) → φ)
Theorem	simp21r 1073	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ ((φ ∧ ψ) ∧ χ ∧ θ) ∧ η) → ψ)
Theorem	simp22l 1074	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ (φ ∧ ψ) ∧ θ) ∧ η) → φ)
Theorem	simp22r 1075	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ (φ ∧ ψ) ∧ θ) ∧ η) → ψ)
Theorem	simp23l 1076	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ θ ∧ (φ ∧ ψ)) ∧ η) → φ)
Theorem	simp23r 1077	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ (χ ∧ θ ∧ (φ ∧ ψ)) ∧ η) → ψ)
Theorem	simp31l 1078	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ ((φ ∧ ψ) ∧ χ ∧ θ)) → φ)
Theorem	simp31r 1079	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ ((φ ∧ ψ) ∧ χ ∧ θ)) → ψ)
Theorem	simp32l 1080	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ (χ ∧ (φ ∧ ψ) ∧ θ)) → φ)
Theorem	simp32r 1081	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ (χ ∧ (φ ∧ ψ) ∧ θ)) → ψ)
Theorem	simp33l 1082	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ (χ ∧ θ ∧ (φ ∧ ψ))) → φ)
Theorem	simp33r 1083	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((τ ∧ η ∧ (χ ∧ θ ∧ (φ ∧ ψ))) → ψ)
Theorem	simp111 1084	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ η ∧ ζ) → φ)
Theorem	simp112 1085	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ η ∧ ζ) → ψ)
Theorem	simp113 1086	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ η ∧ ζ) → χ)
Theorem	simp121 1087	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ η ∧ ζ) → φ)
Theorem	simp122 1088	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ η ∧ ζ) → ψ)
Theorem	simp123 1089	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ η ∧ ζ) → χ)
Theorem	simp131 1090	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ η ∧ ζ) → φ)
Theorem	simp132 1091	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ η ∧ ζ) → ψ)
Theorem	simp133 1092	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ η ∧ ζ) → χ)
Theorem	simp211 1093	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ ζ) → φ)
Theorem	simp212 1094	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ ζ) → ψ)
Theorem	simp213 1095	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ) ∧ ζ) → χ)
Theorem	simp221 1096	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ ζ) → φ)
Theorem	simp222 1097	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ ζ) → ψ)
Theorem	simp223 1098	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ) ∧ ζ) → χ)
Theorem	simp231 1099	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ ζ) → φ)
Theorem	simp232 1100	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ ζ) → ψ)