![]() |
Metamath
Proof Explorer Theorem List (p. 440 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | e212 43901 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee212 43902 | e212 43901 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e122 43903 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e112 43904 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee112 43905 | e112 43904 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e121 43906 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e211 43907 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee211 43908 | e211 43907 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e210 43909 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee210 43910 | e210 43909 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e201 43911 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee201 43912 | e201 43911 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e120 43913 | A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee120 43914 | Virtual deduction rule e120 43913 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||
Theorem | e021 43915 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee021 43916 | e021 43915 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → 𝜏) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e012 43917 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee012 43918 | e012 43917 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜃 → 𝜂)) | ||
Theorem | e102 43919 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee102 43920 | e102 43919 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e22 43921 | A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e22an 43922 | Conjunction form of e22 43921. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee22an 43923 | e22an 43922 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e111 43924 | A virtual deduction elimination rule (see syl3c 66). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | e1111 43925 | A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))) ⇒ ⊢ ( 𝜑 ▶ 𝜂 ) | ||
Theorem | e110 43926 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee110 43927 | e110 43926 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e101 43928 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee101 43929 | e101 43928 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e011 43930 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee011 43931 | e011 43930 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e100 43932 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee100 43933 | e100 43932 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e010 43934 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee010 43935 | e010 43934 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e001 43936 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜒 ▶ 𝜏 ) | ||
Theorem | ee001 43937 | e001 43936 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | e11 43938 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | e11an 43939 | Conjunction form of e11 43938. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee11an 43940 | e11an 43939 without virtual deductions. syl22anc 836 is also e11an 43939 without virtual deductions, exept with a different order of hypotheses. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | e01 43941 | A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | e01an 43942 | Conjunction form of e01 43941. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | ee01an 43943 | e01an 43942 without virtual deductions. sylancr 586 is also a form of e01an 43942 without virtual deduction, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | e10 43944 | A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | e10an 43945 | Conjunction form of e10 43944. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee10an 43946 | e10an 43945 without virtual deductions. sylancl 585 is also e10an 43945 without virtual deductions, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | e02 43947 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e02an 43948 | Conjunction form of e02 43947. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | ee02an 43949 | e02an 43948 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → (𝜒 → 𝜏)) | ||
Theorem | eel021old 43950 | el021old 43951 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜏) | ||
Theorem | el021old 43951 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( ( 𝜓 , 𝜒 ) ▶ 𝜃 ) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( ( 𝜓 , 𝜒 ) ▶ 𝜏 ) | ||
Theorem | eel132 43952 | syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂) | ||
Theorem | eel000cT 43953 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (⊤ → 𝜃) | ||
Theorem | eel0TT 43954 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (⊤ → 𝜓) & ⊢ (⊤ → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelT00 43955 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelTTT 43956 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ (⊤ → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelT11 43957 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | eelT1 43958 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Alan Sare, 23-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | eelT12 43959 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜃 → 𝜏) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | eelTT1 43960 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eelT01 43961 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eel0T1 43962 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (⊤ → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eel12131 43963 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | eel2131 43964 | syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | eel3132 43965 | syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜏) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜂) | ||
Theorem | eel0321old 43966 | el0321old 43967 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜂) | ||
Theorem | el0321old 43967 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜂 ) | ||
Theorem | eel2122old 43968 | el2122old 43969 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜓 → 𝜏) & ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | ||
Theorem | el2122old 43969 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) & ⊢ ( 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜂 ) | ||
Theorem | eel0000 43970 | Elimination rule similar to mp4an 690, except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ 𝜏 | ||
Theorem | eel00001 43971 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜏 → 𝜂) & ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜏 → 𝜁) | ||
Theorem | eel00000 43972 | Elimination rule similar eel0000 43970, except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ 𝜂 | ||
Theorem | eel11111 43973 | Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1379 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | e12 43974 | A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e12an 43975 | Conjunction form of e12 43974 (see syl6an 681). (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) | ||
Theorem | el12 43976 | Virtual deduction form of syl2an 595. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜏 ▶ 𝜒 ) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( ( 𝜑 , 𝜏 ) ▶ 𝜃 ) | ||
Theorem | e20 43977 | A virtual deduction elimination rule (see syl6mpi 67). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e20an 43978 | Conjunction form of e20 43977. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee20an 43979 | e20an 43978 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e21 43980 | A virtual deduction elimination rule (see syl6ci 71). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e21an 43981 | Conjunction form of e21 43980. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee21an 43982 | e21an 43981 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e333 43983 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) | ||
Theorem | e33 43984 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e33an 43985 | Conjunction form of e33 43984. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee33an 43986 | e33an 43985 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e3 43987 | Meta-connective form of syl8 76. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e3bi 43988 | Biconditional form of e3 43987. syl8ib 256 is e3bi 43988 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜃 ↔ 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e3bir 43989 | Right biconditional form of e3 43987. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜏 ↔ 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e03 43990 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03 43991 | e03 43990 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e03an 43992 | Conjunction form of e03 43990. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03an 43993 | Conjunction form of ee03 43991. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e30 43994 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30 43995 | e30 43994 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e30an 43996 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30an 43997 | Conjunction form of ee30 43995. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e13 43998 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | e13an 43999 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee13an 44000 | e13an 43999 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |