Description: An inference based on modus ponens. (Contributed by NM, 19-Oct-2007)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mp3anr3.1 | ⊢ 𝜃 | |
mp3anr3.2 | ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜏 ) | ||
Assertion | mp3anr3 | ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜏 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3anr3.1 | ⊢ 𝜃 | |
2 | mp3anr3.2 | ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜏 ) | |
3 | 2 | ancoms | ⊢ ( ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ∧ 𝜑 ) → 𝜏 ) |
4 | 1 3 | mp3anl3 | ⊢ ( ( ( 𝜓 ∧ 𝜒 ) ∧ 𝜑 ) → 𝜏 ) |
5 | 4 | ancoms | ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜏 ) |