Theorem List for Intuitionistic Logic Explorer - 1001-1100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | simp1i 1001 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜑 |
|
Theorem | simp2i 1002 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜓 |
|
Theorem | simp3i 1003 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜒 |
|
Theorem | simp1d 1004 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | simp2d 1005 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | simp3d 1006 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |
|
Theorem | simp1bi 1007 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | simp2bi 1008 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | simp3bi 1009 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |
|
Theorem | 3adant1 1010 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3adant2 1011 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) |
|
Theorem | 3adant3 1012 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
|
Theorem | 3ad2ant1 1013 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
|
Theorem | 3ad2ant2 1014 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒) |
|
Theorem | 3ad2ant3 1015 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒) |
|
Theorem | simp1l 1016 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) |
|
Theorem | simp1r 1017 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) |
|
Theorem | simp2l 1018 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
|
Theorem | simp2r 1019 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
|
Theorem | simp3l 1020 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) |
|
Theorem | simp3r 1021 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) |
|
Theorem | simp11 1022 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
|
Theorem | simp12 1023 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
|
Theorem | simp13 1024 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) |
|
Theorem | simp21 1025 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
|
Theorem | simp22 1026 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) |
|
Theorem | simp23 1027 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) |
|
Theorem | simp31 1028 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒) |
|
Theorem | simp32 1029 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃) |
|
Theorem | simp33 1030 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏) |
|
Theorem | simpll1 1031 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
|
Theorem | simpll2 1032 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
|
Theorem | simpll3 1033 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) |
|
Theorem | simplr1 1034 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
|
Theorem | simplr2 1035 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) |
|
Theorem | simplr3 1036 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) |
|
Theorem | simprl1 1037 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
|
Theorem | simprl2 1038 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
|
Theorem | simprl3 1039 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
|
Theorem | simprr1 1040 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
|
Theorem | simprr2 1041 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
|
Theorem | simprr3 1042 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
|
Theorem | simpl1l 1043 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) |
|
Theorem | simpl1r 1044 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
|
Theorem | simpl2l 1045 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
|
Theorem | simpl2r 1046 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
|
Theorem | simpl3l 1047 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) |
|
Theorem | simpl3r 1048 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) |
|
Theorem | simpr1l 1049 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
|
Theorem | simpr1r 1050 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
|
Theorem | simpr2l 1051 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
|
Theorem | simpr2r 1052 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
|
Theorem | simpr3l 1053 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
|
Theorem | simpr3r 1054 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
|
Theorem | simp1ll 1055 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
|
Theorem | simp1lr 1056 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
|
Theorem | simp1rl 1057 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
|
Theorem | simp1rr 1058 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
|
Theorem | simp2ll 1059 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) |
|
Theorem | simp2lr 1060 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) |
|
Theorem | simp2rl 1061 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) |
|
Theorem | simp2rr 1062 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) |
|
Theorem | simp3ll 1063 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
|
Theorem | simp3lr 1064 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) |
|
Theorem | simp3rl 1065 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
|
Theorem | simp3rr 1066 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
|
Theorem | simpl11 1067 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑) |
|
Theorem | simpl12 1068 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) |
|
Theorem | simpl13 1069 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) |
|
Theorem | simpl21 1070 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
|
Theorem | simpl22 1071 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
|
Theorem | simpl23 1072 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) |
|
Theorem | simpl31 1073 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) |
|
Theorem | simpl32 1074 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
|
Theorem | simpl33 1075 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) |
|
Theorem | simpr11 1076 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) |
|
Theorem | simpr12 1077 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) |
|
Theorem | simpr13 1078 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) |
|
Theorem | simpr21 1079 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) |
|
Theorem | simpr22 1080 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) |
|
Theorem | simpr23 1081 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) |
|
Theorem | simpr31 1082 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
|
Theorem | simpr32 1083 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
|
Theorem | simpr33 1084 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
|
Theorem | simp1l1 1085 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) |
|
Theorem | simp1l2 1086 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
|
Theorem | simp1l3 1087 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒) |
|
Theorem | simp1r1 1088 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜑) |
|
Theorem | simp1r2 1089 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
|
Theorem | simp1r3 1090 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜒) |
|
Theorem | simp2l1 1091 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜑) |
|
Theorem | simp2l2 1092 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
|
Theorem | simp2l3 1093 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜒) |
|
Theorem | simp2r1 1094 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) |
|
Theorem | simp2r2 1095 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) |
|
Theorem | simp2r3 1096 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) |
|
Theorem | simp3l1 1097 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
|
Theorem | simp3l2 1098 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
|
Theorem | simp3l3 1099 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
|
Theorem | simp3r1 1100 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |