![]() |
Metamath
Proof Explorer Theorem List (p. 436 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ee212 43501 | e212 43500 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e122 43502 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e112 43503 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee112 43504 | e112 43503 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e121 43505 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e211 43506 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee211 43507 | e211 43506 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e210 43508 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee210 43509 | e210 43508 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ 𝜏 & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e201 43510 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜂 ) | ||
Theorem | ee201 43511 | e201 43510 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ (𝜑 → 𝜏) & ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜂)) | ||
Theorem | e120 43512 | A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee120 43513 | Virtual deduction rule e120 43512 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ 𝜏 & ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜂)) | ||
Theorem | e021 43514 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee021 43515 | e021 43514 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜓 → 𝜏) & ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜒 → 𝜂)) | ||
Theorem | e012 43516 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee012 43517 | e012 43516 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜓 → (𝜃 → 𝜂)) | ||
Theorem | e102 43518 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ ( 𝜑 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee102 43519 | e102 43518 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂))) ⇒ ⊢ (𝜑 → (𝜃 → 𝜂)) | ||
Theorem | e22 43520 | A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e22an 43521 | Conjunction form of e22 43520. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee22an 43522 | e22an 43521 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e111 43523 | 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 43524 | A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))) ⇒ ⊢ ( 𝜑 ▶ 𝜂 ) | ||
Theorem | e110 43525 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee110 43526 | e110 43525 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e101 43527 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee101 43528 | e101 43527 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e011 43529 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜓 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee011 43530 | e011 43529 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e100 43531 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜑 ▶ 𝜏 ) | ||
Theorem | ee100 43532 | e100 43531 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | e010 43533 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜓 ▶ 𝜏 ) | ||
Theorem | ee010 43534 | e010 43533 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ 𝜃 & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | e001 43535 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ ( 𝜒 ▶ 𝜏 ) | ||
Theorem | ee001 43536 | e001 43535 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | e11 43537 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | e11an 43538 | Conjunction form of e11 43537. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee11an 43539 | e11an 43538 without virtual deductions. syl22anc 837 is also e11an 43538 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 43540 | A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | e01an 43541 | Conjunction form of e01 43540. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | ee01an 43542 | e01an 43541 without virtual deductions. sylancr 587 is also a form of e01an 43541 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 43543 | 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 43544 | Conjunction form of e10 43543. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee10an 43545 | e10an 43544 without virtual deductions. sylancl 586 is also e10an 43544 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 43546 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e02an 43547 | Conjunction form of e02 43546. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | ee02an 43548 | e02an 43547 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → (𝜒 → 𝜏)) | ||
Theorem | eel021old 43549 | el021old 43550 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜏) | ||
Theorem | el021old 43550 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( ( 𝜓 , 𝜒 ) ▶ 𝜃 ) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( ( 𝜓 , 𝜒 ) ▶ 𝜏 ) | ||
Theorem | eel132 43551 | syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂) | ||
Theorem | eel000cT 43552 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (⊤ → 𝜃) | ||
Theorem | eel0TT 43553 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (⊤ → 𝜓) & ⊢ (⊤ → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelT00 43554 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelTTT 43555 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ (⊤ → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelT11 43556 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | eelT1 43557 | 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 43558 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜃 → 𝜏) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | eelTT1 43559 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eelT01 43560 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eel0T1 43561 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (⊤ → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eel12131 43562 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | eel2131 43563 | syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | eel3132 43564 | syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜏) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜂) | ||
Theorem | eel0321old 43565 | el0321old 43566 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜂) | ||
Theorem | el0321old 43566 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜂 ) | ||
Theorem | eel2122old 43567 | el2122old 43568 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜓 → 𝜏) & ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | ||
Theorem | el2122old 43568 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) & ⊢ ( 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜂 ) | ||
Theorem | eel0000 43569 | Elimination rule similar to mp4an 691, except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ 𝜏 | ||
Theorem | eel00001 43570 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜏 → 𝜂) & ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜏 → 𝜁) | ||
Theorem | eel00000 43571 | Elimination rule similar eel0000 43569, except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ 𝜂 | ||
Theorem | eel11111 43572 | Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1382 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | e12 43573 | 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 43574 | Conjunction form of e12 43573 (see syl6an 682). (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) | ||
Theorem | el12 43575 | Virtual deduction form of syl2an 596. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜏 ▶ 𝜒 ) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( ( 𝜑 , 𝜏 ) ▶ 𝜃 ) | ||
Theorem | e20 43576 | 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 43577 | Conjunction form of e20 43576. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee20an 43578 | e20an 43577 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e21 43579 | 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 43580 | Conjunction form of e21 43579. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee21an 43581 | e21an 43580 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e333 43582 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) | ||
Theorem | e33 43583 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e33an 43584 | Conjunction form of e33 43583. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee33an 43585 | e33an 43584 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e3 43586 | Meta-connective form of syl8 76. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e3bi 43587 | Biconditional form of e3 43586. syl8ib 255 is e3bi 43587 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜃 ↔ 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e3bir 43588 | Right biconditional form of e3 43586. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜏 ↔ 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e03 43589 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03 43590 | e03 43589 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e03an 43591 | Conjunction form of e03 43589. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03an 43592 | Conjunction form of ee03 43590. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e30 43593 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30 43594 | e30 43593 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e30an 43595 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30an 43596 | Conjunction form of ee30 43594. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e13 43597 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | e13an 43598 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee13an 43599 | e13an 43598 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e31 43600 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |