|   | Mathbox for Richard Penner | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > frege5 | Structured version Visualization version GIF version | ||
| Description: A closed form of syl 17. Identical to imim2 58. Theorem *2.05 of [WhiteheadRussell] p. 100. Proposition 5 of [Frege1879] p. 32. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) | 
| Ref | Expression | 
|---|---|
| frege5 | ⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ax-frege1 43808 | . 2 ⊢ ((𝜑 → 𝜓) → (𝜒 → (𝜑 → 𝜓))) | |
| 2 | frege4 43817 | . 2 ⊢ (((𝜑 → 𝜓) → (𝜒 → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 | 
| This theorem was proved from axioms: ax-mp 5 ax-frege1 43808 ax-frege2 43809 | 
| This theorem is referenced by: rp-frege25 43823 frege6 43824 frege7 43826 frege9 43830 frege12 43831 frege16 43834 frege25 43835 frege18 43836 frege22 43837 frege14 43841 frege29 43849 frege34 43855 frege45 43867 frege80 43961 frege90 43971 | 
| Copyright terms: Public domain | W3C validator |