![]() |
Metamath
Proof Explorer Theorem List (p. 442 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vd13 44101 | 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 44102 | 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 44103 | 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 44104 | 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 44105 | 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 44106 | The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. Conventional form of int2 44106 is ex 411. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 ▶ (𝜓 → 𝜒) ) | ||
Theorem | iin2 44107 | in2 44105 without virtual deductions. (Contributed by Alan Sare, 20-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | in2an 44108 | The virtual deduction introduction rule converting the second conjunct of the second virtual hypothesis into the antecedent of the conclusion. expd 414 is the non-virtual deduction form of in2an 44108. (Contributed by Alan Sare, 30-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , (𝜓 ∧ 𝜒) ▶ 𝜃 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ (𝜒 → 𝜃) ) | ||
Theorem | in3 44109 | 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 44110 | in3 44109 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 44111 | The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a 430 is the non-virtual deduction form of in3an 44111. (Contributed by Alan Sare, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , (𝜒 ∧ 𝜃) ▶ 𝜏 ) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ (𝜃 → 𝜏) ) | ||
Theorem | int3 44112 | The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. Conventional form of int3 44112 is 3expia 1118. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 , 𝜒 ) ▶ 𝜃 ) ⇒ ⊢ ( ( 𝜑 , 𝜓 ) ▶ (𝜒 → 𝜃) ) | ||
Theorem | idn2 44113 | 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 44114 | Virtual deduction identity rule. simpr 483 in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜓 ) | ||
Theorem | idn3 44115 | 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 44116* | Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1922 is gen11 44116 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) | ||
Theorem | gen11nv 44117 | Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis without distinct variables. alrimih 1818 is gen11nv 44117 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) | ||
Theorem | gen12 44118* | Virtual deduction generalizing rule for two quantifying variables and one virtual hypothesis. gen12 44118 is alrimivv 1923 with virtual deductions. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ ∀𝑥∀𝑦𝜓 ) | ||
Theorem | gen21 44119* | Virtual deduction generalizing rule for one quantifying variables and two virtual hypothesis. gen21 44119 is alrimdv 1924 with virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ ∀𝑥𝜒 ) | ||
Theorem | gen21nv 44120 | Virtual deduction form of alrimdh 1858. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ ∀𝑥𝜒 ) | ||
Theorem | gen31 44121* | Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 44121 is ggen31 44045 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ ∀𝑥𝜃 ) | ||
Theorem | gen22 44122* | 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 44123* | gen22 44122 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | exinst 44124 | Existential Instantiation. Virtual deduction form of exlimexi 44024. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ ( ∃𝑥𝜑 , 𝜑 ▶ 𝜓 ) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
Theorem | exinst01 44125 | 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 44126 | 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 44127 | A Virtual deduction elimination rule. syl 17 is e1a 44127 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | el1 44128 | A Virtual deduction elimination rule. syl 17 is el1 44128 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | e1bi 44129 | Biconditional form of e1a 44127. sylib 217 is e1bi 44129 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | e1bir 44130 | Right biconditional form of e1a 44127. sylibr 233 is e1bir 44130 without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ ( 𝜑 ▶ 𝜒 ) | ||
Theorem | e2 44131 | A virtual deduction elimination rule. syl6 35 is e2 44131 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
Theorem | e2bi 44132 | Biconditional form of e2 44131. imbitrdi 250 is e2bi 44132 without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
Theorem | e2bir 44133 | Right biconditional form of e2 44131. imbitrrdi 251 is e2bir 44133 without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ (𝜃 ↔ 𝜒) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) | ||
Theorem | ee223 44134 | e223 44135 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) & ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜁))) | ||
Theorem | e223 44135 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜏 ▶ 𝜁 ) | ||
Theorem | e222 44136 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | e220 44137 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee220 44138 | e220 44137 without virtual deductions. (Contributed by Alan Sare, 12-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e202 44139 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee202 44140 | e202 44139 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e022 44141 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee022 44142 | e022 44141 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → (𝜒 → 𝜏)) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e002 44143 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ( 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee002 44144 | e002 44143 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜒 → (𝜃 → 𝜂)) | ||
Theorem | e020 44145 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee020 44146 | e020 44145 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e200 44147 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee200 44148 | e200 44147 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e221 44149 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee221 44150 | e221 44149 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e212 44151 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee212 44152 | e212 44151 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e122 44153 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e112 44154 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee112 44155 | e112 44154 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e121 44156 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e211 44157 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee211 44158 | e211 44157 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e210 44159 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee210 44160 | e210 44159 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e201 44161 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee201 44162 | e201 44161 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e120 44163 | A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee120 44164 | Virtual deduction rule e120 44163 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||
Theorem | e021 44165 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee021 44166 | e021 44165 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → 𝜏) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e012 44167 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee012 44168 | e012 44167 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜃 → 𝜂)) | ||
Theorem | e102 44169 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee102 44170 | e102 44169 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e22 44171 | A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e22an 44172 | Conjunction form of e22 44171. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee22an 44173 | e22an 44172 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e111 44174 | 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 44175 | A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))) ⇒ ⊢ ( 𝜑 ▶ 𝜂 ) | ||
Theorem | e110 44176 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee110 44177 | e110 44176 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e101 44178 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee101 44179 | e101 44178 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e011 44180 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee011 44181 | e011 44180 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e100 44182 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee100 44183 | e100 44182 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e010 44184 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee010 44185 | e010 44184 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e001 44186 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜒 ▶ 𝜏 ) | ||
Theorem | ee001 44187 | e001 44186 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | e11 44188 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | e11an 44189 | Conjunction form of e11 44188. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee11an 44190 | e11an 44189 without virtual deductions. syl22anc 837 is also e11an 44189 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 44191 | A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | e01an 44192 | Conjunction form of e01 44191. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | ee01an 44193 | e01an 44192 without virtual deductions. sylancr 585 is also a form of e01an 44192 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 44194 | 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 44195 | Conjunction form of e10 44194. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee10an 44196 | e10an 44195 without virtual deductions. sylancl 584 is also e10an 44195 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 44197 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e02an 44198 | Conjunction form of e02 44197. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | ee02an 44199 | e02an 44198 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → (𝜒 → 𝜏)) | ||
Theorem | eel021old 44200 | el021old 44201 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜏) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |