Description: A kind of Aristotelian inference. This judgement replaces the mode of inference barbara when the minor premise has a particular context. Proposition 62 of Frege1879 p. 52. (Contributed by RP, 17-Apr-2020) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | frege62a | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜃 ) → ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜃 → 𝜏 ) ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frege58acor | ⊢ ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜃 → 𝜏 ) ) → ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) | |
| 2 | ax-frege8 | ⊢ ( ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜃 → 𝜏 ) ) → ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) → ( if- ( 𝜑 , 𝜓 , 𝜃 ) → ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜃 → 𝜏 ) ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) ) | |
| 3 | 1 2 | ax-mp | ⊢ ( if- ( 𝜑 , 𝜓 , 𝜃 ) → ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜃 → 𝜏 ) ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ) |