| Metamath
Proof Explorer Theorem List (p. 447 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-vhc2 44601 | Definition of a 2-element virtual hypotheses collection. (Contributed by Alan Sare, 23-Apr-2015.) (New usage is discouraged.) |
| ⊢ (( 𝜑 , 𝜓 ) ↔ (𝜑 ∧ 𝜓)) | ||
| Theorem | dfvd2an 44602 | Definition of a 2-hypothesis virtual deduction in vd conjunction form. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) ↔ ((𝜑 ∧ 𝜓) → 𝜒)) | ||
| Theorem | dfvd2ani 44603 | Inference form of dfvd2an 44602. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
| Theorem | dfvd2anir 44604 | Right-to-left inference form of dfvd2an 44602. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) | ||
| Theorem | dfvd2i 44605 | Inference form of dfvd2 44599. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
| Theorem | dfvd2ir 44606 | Right-to-left inference form of dfvd2 44599. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | ||
| Syntax | wvd3 44607 | Syntax for a 3-hypothesis virtual deduction. (New usage is discouraged.) |
| wff ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) | ||
| Syntax | wvhc3 44608 | Syntax for a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.) |
| wff ( 𝜑 , 𝜓 , 𝜒 ) | ||
| Definition | df-vhc3 44609 | Definition of a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.) |
| ⊢ (( 𝜑 , 𝜓 , 𝜒 ) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
| Definition | df-vd3 44610 | Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (New usage is discouraged.) |
| ⊢ (( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)) | ||
| Theorem | dfvd3 44611 | Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃)))) | ||
| Theorem | dfvd3i 44612 | Inference form of dfvd3 44611. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
| Theorem | dfvd3ir 44613 | Right-to-left inference form of dfvd3 44611. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) | ||
| Theorem | dfvd3an 44614 | 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 44615 | Inference form of dfvd3an 44614. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | dfvd3anir 44616 | Right-to-left inference form of dfvd3an 44614. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) | ||
| Theorem | vd01 44617 | A virtual hypothesis virtually infers a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 ⇒ ⊢ ( 𝜓 ▶ 𝜑 ) | ||
| Theorem | vd02 44618 | Two virtual hypotheses virtually infer a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜑 ) | ||
| Theorem | vd03 44619 | 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 44620 | 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 44621 | 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 44622 | 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 44623 | 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 44624 | 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 44625 | 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 44626 | The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. Conventional form of int2 44626 is ex 412. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) | ||
| Theorem | iin2 44627 | in2 44625 without virtual deductions. (Contributed by Alan Sare, 20-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
| Theorem | in2an 44628 | The virtual deduction introduction rule converting the second conjunct of the second virtual hypothesis into the antecedent of the conclusion. expd 415 is the non-virtual deduction form of in2an 44628. (Contributed by Alan Sare, 30-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , (𝜓 ∧ 𝜒) ▶ 𝜃 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ (𝜒 → 𝜃) ) | ||
| Theorem | in3 44629 | 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 44630 | in3 44629 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 44631 | The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a 431 is the non-virtual deduction form of in3an 44631. (Contributed by Alan Sare, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 , (𝜒 ∧ 𝜃) ▶ 𝜏 ) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ (𝜃 → 𝜏) ) | ||
| Theorem | int3 44632 | The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. Conventional form of int3 44632 is 3expia 1122. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) ⇒ ⊢ ( ( 𝜑 , 𝜓 ) ▶ (𝜒 → 𝜃) ) | ||
| Theorem | idn2 44633 | 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 44634 | Virtual deduction identity rule. simpr 484 in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜓 ) | ||
| Theorem | idn3 44635 | 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 44636* | Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1927 is gen11 44636 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) | ||
| Theorem | gen11nv 44637 | Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis without distinct variables. alrimih 1824 is gen11nv 44637 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) | ||
| Theorem | gen12 44638* | Virtual deduction generalizing rule for two quantifying variables and one virtual hypothesis. gen12 44638 is alrimivv 1928 with virtual deductions. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥∀𝑦𝜓 ) | ||
| Theorem | gen21 44639* | Virtual deduction generalizing rule for one quantifying variables and two virtual hypothesis. gen21 44639 is alrimdv 1929 with virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ ∀𝑥𝜒 ) | ||
| Theorem | gen21nv 44640 | Virtual deduction form of alrimdh 1863. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ ∀𝑥𝜒 ) | ||
| Theorem | gen31 44641* | Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 44641 is ggen31 44565 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ ∀𝑥𝜃 ) | ||
| Theorem | gen22 44642* | 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 44643* | gen22 44642 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥∀𝑦𝜒)) | ||
| Theorem | exinst 44644 | Existential Instantiation. Virtual deduction form of exlimexi 44544. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ ( ∃𝑥𝜑 , 𝜑 ▶ 𝜓 ) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
| Theorem | exinst01 44645 | 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 44646 | 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 44647 | A Virtual deduction elimination rule. syl 17 is e1a 44647 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
| Theorem | el1 44648 | A Virtual deduction elimination rule. syl 17 is el1 44648 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
| Theorem | e1bi 44649 | Biconditional form of e1a 44647. sylib 218 is e1bi 44649 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
| Theorem | e1bir 44650 | Right biconditional form of e1a 44647. sylibr 234 is e1bir 44650 without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
| Theorem | e2 44651 | A virtual deduction elimination rule. syl6 35 is e2 44651 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
| Theorem | e2bi 44652 | Biconditional form of e2 44651. imbitrdi 251 is e2bi 44652 without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
| Theorem | e2bir 44653 | Right biconditional form of e2 44651. imbitrrdi 252 is e2bir 44653 without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
| Theorem | ee223 44654 | e223 44655 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) & ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜁))) | ||
| Theorem | e223 44655 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜏 ▶ 𝜁 ) | ||
| Theorem | e222 44656 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | e220 44657 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee220 44658 | e220 44657 without virtual deductions. (Contributed by Alan Sare, 12-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e202 44659 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee202 44660 | e202 44659 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e022 44661 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
| Theorem | ee022 44662 | e022 44661 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → (𝜒 → 𝜏)) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
| Theorem | e002 44663 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ 𝜓 & ⊢ ( 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜒 , 𝜃 ▶ 𝜂 ) | ||
| Theorem | ee002 44664 | e002 44663 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜒 → (𝜃 → 𝜂)) | ||
| Theorem | e020 44665 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
| Theorem | ee020 44666 | e020 44665 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
| Theorem | e200 44667 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee200 44668 | e200 44667 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e221 44669 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee221 44670 | e221 44669 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e212 44671 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee212 44672 | e212 44671 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e122 44673 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
| Theorem | e112 44674 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
| Theorem | ee112 44675 | e112 44674 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
| Theorem | e121 44676 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
| Theorem | e211 44677 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee211 44678 | e211 44677 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e210 44679 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee210 44680 | e210 44679 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e201 44681 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
| Theorem | ee201 44682 | e201 44681 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
| Theorem | e120 44683 | A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
| Theorem | ee120 44684 | Virtual deduction rule e120 44683 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||
| Theorem | e021 44685 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
| Theorem | ee021 44686 | e021 44685 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → 𝜏) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
| Theorem | e012 44687 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜃 ▶ 𝜂 ) | ||
| Theorem | ee012 44688 | e012 44687 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜃 → 𝜂)) | ||
| Theorem | e102 44689 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
| Theorem | ee102 44690 | e102 44689 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
| Theorem | e22 44691 | A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
| Theorem | e22an 44692 | Conjunction form of e22 44691. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
| Theorem | ee22an 44693 | e22an 44692 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
| Theorem | e111 44694 | 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 44695 | A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))) ⇒ ⊢ ( 𝜑 ▶ 𝜂 ) | ||
| Theorem | e110 44696 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
| Theorem | ee110 44697 | e110 44696 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
| Theorem | e101 44698 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
| Theorem | ee101 44699 | e101 44698 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
| Theorem | e011 44700 | 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 > |