Description: Theorem *5.31 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | pm5.31 | ⊢ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | ⊢ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) | |
2 | simpl | ⊢ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → 𝜒 ) | |
3 | 1 2 | jctird | ⊢ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) ) |