HomeTheorem List (p. 10 of 102)
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. 10 of 102) | < 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 | 3simpa 901 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) | ||
| Theorem | 3simpb 902 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) | ||
| Theorem | 3simpc 903 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | ||
| Theorem | simp1 904 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | ||
| Theorem | simp2 905 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | ||
| Theorem | simp3 906 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | ||
| Theorem | simpl1 907 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | ||
| Theorem | simpl2 908 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
| Theorem | simpl3 909 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
| Theorem | simpr1 910 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
| Theorem | simpr2 911 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) | ||
| Theorem | simpr3 912 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) | ||
| Theorem | simp1i 913 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
| ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜑 | ||
| Theorem | simp2i 914 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
| ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜓 | ||
| Theorem | simp3i 915 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
| ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜒 | ||
| Theorem | simp1d 916 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
| ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | simp2d 917 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
| ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
| Theorem | simp3d 918 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
| ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
| Theorem | simp1bi 919 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | simp2bi 920 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
| Theorem | simp3bi 921 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
| Theorem | 3adant1 922 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒) | ||
| Theorem | 3adant2 923 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) | ||
| Theorem | 3adant3 924 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
| Theorem | 3ad2ant1 925 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
| ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
| Theorem | 3ad2ant2 926 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
| ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒) | ||
| Theorem | 3ad2ant3 927 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
| ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒) | ||
| Theorem | simp1l 928 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
| Theorem | simp1r 929 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
| Theorem | simp2l 930 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
| Theorem | simp2r 931 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
| Theorem | simp3l 932 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) | ||
| Theorem | simp3r 933 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) | ||
| Theorem | simp11 934 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
| Theorem | simp12 935 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
| Theorem | simp13 936 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) | ||
| Theorem | simp21 937 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simp22 938 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
| Theorem | simp23 939 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) | ||
| Theorem | simp31 940 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
| Theorem | simp32 941 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃) | ||
| Theorem | simp33 942 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏) | ||
| Theorem | simpll1 943 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpll2 944 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpll3 945 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
| Theorem | simplr1 946 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) | ||
| Theorem | simplr2 947 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) | ||
| Theorem | simplr3 948 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | ||
| Theorem | simprl1 949 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simprl2 950 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simprl3 951 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
| Theorem | simprr1 952 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simprr2 953 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simprr3 954 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | simpl1l 955 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpl1r 956 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpl2l 957 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpl2r 958 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpl3l 959 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
| Theorem | simpl3r 960 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
| Theorem | simpr1l 961 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
| Theorem | simpr1r 962 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
| Theorem | simpr2l 963 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simpr2r 964 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simpr3l 965 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
| Theorem | simpr3r 966 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
| Theorem | simp1ll 967 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
| Theorem | simp1lr 968 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
| Theorem | simp1rl 969 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
| Theorem | simp1rr 970 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
| Theorem | simp2ll 971 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) | ||
| Theorem | simp2lr 972 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) | ||
| Theorem | simp2rl 973 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜑) | ||
| Theorem | simp2rr 974 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏) → 𝜓) | ||
| Theorem | simp3ll 975 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) | ||
| Theorem | simp3lr 976 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) | ||
| Theorem | simp3rl 977 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
| Theorem | simp3rr 978 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
| Theorem | simpl11 979 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl12 980 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl13 981 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpl21 982 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl22 983 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl23 984 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpl31 985 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl32 986 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl33 987 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpr11 988 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) | ||
| Theorem | simpr12 989 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) | ||
| Theorem | simpr13 990 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
| Theorem | simpr21 991 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) | ||
| Theorem | simpr22 992 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) | ||
| Theorem | simpr23 993 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) | ||
| Theorem | simpr31 994 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simpr32 995 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simpr33 996 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | simp1l1 997 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp1l2 998 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp1l3 999 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
| Theorem | simp1r1 1000 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |