Metamath Proof Explorer


Theorem syl3anr1

Description: A syllogism inference. (Contributed by NM, 31-Jul-2007)

Ref Expression
Hypotheses syl3anr1.1 ( 𝜑𝜓 )
syl3anr1.2 ( ( 𝜒 ∧ ( 𝜓𝜃𝜏 ) ) → 𝜂 )
Assertion syl3anr1 ( ( 𝜒 ∧ ( 𝜑𝜃𝜏 ) ) → 𝜂 )

Proof

Step Hyp Ref Expression
1 syl3anr1.1 ( 𝜑𝜓 )
2 syl3anr1.2 ( ( 𝜒 ∧ ( 𝜓𝜃𝜏 ) ) → 𝜂 )
3 1 3anim1i ( ( 𝜑𝜃𝜏 ) → ( 𝜓𝜃𝜏 ) )
4 3 2 sylan2 ( ( 𝜒 ∧ ( 𝜑𝜃𝜏 ) ) → 𝜂 )