Description: Lemma for frege65a . Proposition 64 of Frege1879 p. 53. (Contributed by RP, 17-Apr-2020) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | frege64a | ⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜏 ) → if- ( 𝜎 , 𝜒 , 𝜂 ) ) → ( ( ( 𝜒 → 𝜃 ) ∧ ( 𝜂 → 𝜁 ) ) → ( if- ( 𝜑 , 𝜓 , 𝜏 ) → if- ( 𝜎 , 𝜃 , 𝜁 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege62a | ⊢ ( if- ( 𝜎 , 𝜒 , 𝜂 ) → ( ( ( 𝜒 → 𝜃 ) ∧ ( 𝜂 → 𝜁 ) ) → if- ( 𝜎 , 𝜃 , 𝜁 ) ) ) | |
2 | frege18 | ⊢ ( ( if- ( 𝜎 , 𝜒 , 𝜂 ) → ( ( ( 𝜒 → 𝜃 ) ∧ ( 𝜂 → 𝜁 ) ) → if- ( 𝜎 , 𝜃 , 𝜁 ) ) ) → ( ( if- ( 𝜑 , 𝜓 , 𝜏 ) → if- ( 𝜎 , 𝜒 , 𝜂 ) ) → ( ( ( 𝜒 → 𝜃 ) ∧ ( 𝜂 → 𝜁 ) ) → ( if- ( 𝜑 , 𝜓 , 𝜏 ) → if- ( 𝜎 , 𝜃 , 𝜁 ) ) ) ) ) | |
3 | 1 2 | ax-mp | ⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜏 ) → if- ( 𝜎 , 𝜒 , 𝜂 ) ) → ( ( ( 𝜒 → 𝜃 ) ∧ ( 𝜂 → 𝜁 ) ) → ( if- ( 𝜑 , 𝜓 , 𝜏 ) → if- ( 𝜎 , 𝜃 , 𝜁 ) ) ) ) |