Home | Metamath
Proof Explorer Theorem List (p. 409 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | wvd3 40801 | Syntax for a 3-hypothesis virtual deduction. (New usage is discouraged.) |
wff ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) | ||
Syntax | wvhc3 40802 | Syntax for a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.) |
wff ( 𝜑 , 𝜓 , 𝜒 ) | ||
Definition | df-vhc3 40803 | Definition of a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.) |
⊢ (( 𝜑 , 𝜓 , 𝜒 ) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Definition | df-vd3 40804 | Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (New usage is discouraged.) |
⊢ (( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | dfvd3 40805 | Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))) | ||
Theorem | dfvd3i 40806 | Inference form of dfvd3 40805. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | dfvd3ir 40807 | Right-to-left inference form of dfvd3 40805. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) | ||
Theorem | dfvd3an 40808 | Definition of a 3-hypothesis virtual deduction in vd conjunction form. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | dfvd3ani 40809 | Inference form of dfvd3an 40808. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | dfvd3anir 40810 | Right-to-left inference form of dfvd3an 40808. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) | ||
Theorem | vd01 40811 | A virtual hypothesis virtually infers a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 ⇒ ⊢ ( 𝜓 ▶ 𝜑 ) | ||
Theorem | vd02 40812 | Two virtual hypotheses virtually infer a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜑 ) | ||
Theorem | vd03 40813 | A theorem is virtually inferred by the 3 virtual hypotheses. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜑 ) | ||
Theorem | vd12 40814 | A virtual deduction with 1 virtual hypothesis virtually inferring a virtual conclusion infers that the same conclusion is virtually inferred by the same virtual hypothesis and an additional hypothesis. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜓 ) | ||
Theorem | vd13 40815 | A virtual deduction with 1 virtual hypothesis virtually inferring a virtual conclusion infers that the same conclusion is virtually inferred by the same virtual hypothesis and a two additional hypotheses. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜓 ) | ||
Theorem | vd23 40816 | A virtual deduction with 2 virtual hypotheses virtually inferring a virtual conclusion infers that the same conclusion is virtually inferred by the same 2 virtual hypotheses and a third hypothesis. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜒 ) | ||
Theorem | dfvd2imp 40817 | The virtual deduction form of a 2-antecedent nested implication implies the 2-antecedent nested implication. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (( 𝜑 , 𝜓 ▶ 𝜒 ) → (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | dfvd2impr 40818 | A 2-antecedent nested implication implies its virtual deduction form. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ( 𝜑 , 𝜓 ▶ 𝜒 )) | ||
Theorem | in2 40819 | The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) | ||
Theorem | int2 40820 | The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. Conventional form of int2 40820 is ex 413. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) | ||
Theorem | iin2 40821 | in2 40819 without virtual deductions. (Contributed by Alan Sare, 20-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | in2an 40822 | The virtual deduction introduction rule converting the second conjunct of the second virtual hypothesis into the antecedent of the conclusion. expd 416 is the non-virtual deduction form of in2an 40822. (Contributed by Alan Sare, 30-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , (𝜓 ∧ 𝜒) ▶ 𝜃 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ (𝜒 → 𝜃) ) | ||
Theorem | in3 40823 | The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ (𝜒 → 𝜃) ) | ||
Theorem | iin3 40824 | in3 40823 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | in3an 40825 | The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a 432 is the non-virtual deduction form of in3an 40825. (Contributed by Alan Sare, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , (𝜒 ∧ 𝜃) ▶ 𝜏 ) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ (𝜃 → 𝜏) ) | ||
Theorem | int3 40826 | The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. Conventional form of int3 40826 is 3expia 1113. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) ⇒ ⊢ ( ( 𝜑 , 𝜓 ) ▶ (𝜒 → 𝜃) ) | ||
Theorem | idn2 40827 | Virtual deduction identity rule which is idd 24 with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜓 ) | ||
Theorem | iden2 40828 | Virtual deduction identity rule. simpr 485 in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜓 ) | ||
Theorem | idn3 40829 | Virtual deduction identity rule for three virtual hypotheses. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜒 ) | ||
Theorem | gen11 40830* | Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1919 is gen11 40830 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) | ||
Theorem | gen11nv 40831 | Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis without distinct variables. alrimih 1815 is gen11nv 40831 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) | ||
Theorem | gen12 40832* | Virtual deduction generalizing rule for two quantifying variables and one virtual hypothesis. gen12 40832 is alrimivv 1920 with virtual deductions. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥∀𝑦𝜓 ) | ||
Theorem | gen21 40833* | Virtual deduction generalizing rule for one quantifying variables and two virtual hypothesis. gen21 40833 is alrimdv 1921 with virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ ∀𝑥𝜒 ) | ||
Theorem | gen21nv 40834 | Virtual deduction form of alrimdh 1855. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ ∀𝑥𝜒 ) | ||
Theorem | gen31 40835* | Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 40835 is ggen31 40759 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ ∀𝑥𝜃 ) | ||
Theorem | gen22 40836* | Virtual deduction generalizing rule for two quantifying variables and two virtual hypothesis. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ ∀𝑥∀𝑦𝜒 ) | ||
Theorem | ggen22 40837* | gen22 40836 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | exinst 40838 | Existential Instantiation. Virtual deduction form of exlimexi 40738. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ ( ∃𝑥𝜑 , 𝜑 ▶ 𝜓 ) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
Theorem | exinst01 40839 | Existential Instantiation. Virtual Deduction rule corresponding to a special case of the Natural Deduction Sequent Calculus rule called Rule C in [Margaris] p. 79 and E ∃ in Table 1 on page 4 of the paper "Extracting information from intermediate T-systems" (2000) presented at IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑥𝜓 & ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | exinst11 40840 | Existential Instantiation. Virtual Deduction rule corresponding to a special case of the Natural Deduction Sequent Calculus rule called Rule C in [Margaris] p. 79 and E ∃ in Table 1 on page 4 of the paper "Extracting information from intermediate T-systems" (2000) presented at IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ ∃𝑥𝜓 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | e1a 40841 | A Virtual deduction elimination rule. syl 17 is e1a 40841 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | el1 40842 | A Virtual deduction elimination rule. syl 17 is el1 40842 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | e1bi 40843 | Biconditional form of e1a 40841. sylib 219 is e1bi 40843 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | e1bir 40844 | Right biconditional form of e1a 40841. sylibr 235 is e1bir 40844 without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | e2 40845 | A virtual deduction elimination rule. syl6 35 is e2 40845 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
Theorem | e2bi 40846 | Biconditional form of e2 40845. syl6ib 252 is e2bi 40846 without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
Theorem | e2bir 40847 | Right biconditional form of e2 40845. syl6ibr 253 is e2bir 40847 without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
Theorem | ee223 40848 | e223 40849 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) & ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜁))) | ||
Theorem | e223 40849 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜏 ▶ 𝜁 ) | ||
Theorem | e222 40850 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | e220 40851 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee220 40852 | e220 40851 without virtual deductions. (Contributed by Alan Sare, 12-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e202 40853 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee202 40854 | e202 40853 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e022 40855 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee022 40856 | e022 40855 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → (𝜒 → 𝜏)) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e002 40857 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ( 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee002 40858 | e002 40857 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜒 → (𝜃 → 𝜂)) | ||
Theorem | e020 40859 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee020 40860 | e020 40859 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e200 40861 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee200 40862 | e200 40861 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e221 40863 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee221 40864 | e221 40863 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e212 40865 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee212 40866 | e212 40865 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e122 40867 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e112 40868 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee112 40869 | e112 40868 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e121 40870 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e211 40871 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee211 40872 | e211 40871 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e210 40873 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee210 40874 | e210 40873 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e201 40875 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee201 40876 | e201 40875 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e120 40877 | A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee120 40878 | Virtual deduction rule e120 40877 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||
Theorem | e021 40879 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee021 40880 | e021 40879 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → 𝜏) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e012 40881 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee012 40882 | e012 40881 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜃 → 𝜂)) | ||
Theorem | e102 40883 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee102 40884 | e102 40883 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e22 40885 | A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e22an 40886 | Conjunction form of e22 40885. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee22an 40887 | e22an 40886 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e111 40888 | 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 40889 | A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))) ⇒ ⊢ ( 𝜑 ▶ 𝜂 ) | ||
Theorem | e110 40890 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee110 40891 | e110 40890 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e101 40892 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee101 40893 | e101 40892 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e011 40894 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee011 40895 | e011 40894 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e100 40896 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee100 40897 | e100 40896 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e010 40898 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee010 40899 | e010 40898 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e001 40900 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜒 ▶ 𝜏 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |