HomeTheorem List (p. 11 of 138)
GIF version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 11 of 138) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 3adant2 1001 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) | ||
| Theorem | 3adant3 1002 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
| Theorem | 3ad2ant1 1003 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
| ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
| Theorem | 3ad2ant2 1004 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
| ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒) | ||
| Theorem | 3ad2ant3 1005 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
| ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒) | ||
| Theorem | simp1l 1006 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
| Theorem | simp1r 1007 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
| Theorem | simp2l 1008 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
| Theorem | simp2r 1009 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
| Theorem | simp3l 1010 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) | ||
| Theorem | simp3r 1011 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) | ||
| Theorem | simp11 1012 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
| Theorem | simp12 1013 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
| Theorem | simp13 1014 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) | ||
| Theorem | simp21 1015 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simp22 1016 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
| Theorem | simp23 1017 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) | ||
| Theorem | simp31 1018 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
| Theorem | simp32 1019 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃) | ||
| Theorem | simp33 1020 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏) | ||
| Theorem | simpll1 1021 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpll2 1022 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpll3 1023 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
| Theorem | simplr1 1024 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) | ||
| Theorem | simplr2 1025 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) | ||
| Theorem | simplr3 1026 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | ||
| Theorem | simprl1 1027 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simprl2 1028 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simprl3 1029 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
| Theorem | simprr1 1030 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simprr2 1031 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simprr3 1032 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | simpl1l 1033 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpl1r 1034 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpl2l 1035 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpl2r 1036 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpl3l 1037 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpl3r 1038 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpr1l 1039 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
| Theorem | simpr1r 1040 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
| Theorem | simpr2l 1041 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simpr2r 1042 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simpr3l 1043 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
| Theorem | simpr3r 1044 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
| Theorem | simp1ll 1045 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
| Theorem | simp1lr 1046 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
| Theorem | simp1rl 1047 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
| Theorem | simp1rr 1048 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
| Theorem | simp2ll 1049 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) | ||
| Theorem | simp2lr 1050 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) | ||
| Theorem | simp2rl 1051 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
| Theorem | simp2rr 1052 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
| Theorem | simp3ll 1053 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) | ||
| Theorem | simp3lr 1054 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) | ||
| Theorem | simp3rl 1055 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
| Theorem | simp3rr 1056 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
| Theorem | simpl11 1057 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl12 1058 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl13 1059 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpl21 1060 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl22 1061 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl23 1062 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpl31 1063 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl32 1064 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl33 1065 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpr11 1066 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) | ||
| Theorem | simpr12 1067 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) | ||
| Theorem | simpr13 1068 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
| Theorem | simpr21 1069 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) | ||
| Theorem | simpr22 1070 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) | ||
| Theorem | simpr23 1071 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) | ||
| Theorem | simpr31 1072 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simpr32 1073 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simpr33 1074 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | simp1l1 1075 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp1l2 1076 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp1l3 1077 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
| Theorem | simp1r1 1078 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp1r2 1079 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp1r3 1080 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
| Theorem | simp2l1 1081 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp2l2 1082 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp2l3 1083 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜒) | ||
| Theorem | simp2r1 1084 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp2r2 1085 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp2r3 1086 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
| Theorem | simp3l1 1087 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simp3l2 1088 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simp3l3 1089 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
| Theorem | simp3r1 1090 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simp3r2 1091 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simp3r3 1092 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | simp11l 1093 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp11r 1094 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp12l 1095 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp12r 1096 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp13l 1097 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp13r 1098 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp21l 1099 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp21r 1100 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |