Metamath Proof Explorer


Theorem imbitrrid

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994)

Ref Expression
Hypotheses imbitrrid.1 ( 𝜑𝜃 )
imbitrrid.2 ( 𝜒 → ( 𝜓𝜃 ) )
Assertion imbitrrid ( 𝜒 → ( 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 imbitrrid.1 ( 𝜑𝜃 )
2 imbitrrid.2 ( 𝜒 → ( 𝜓𝜃 ) )
3 2 bicomd ( 𝜒 → ( 𝜃𝜓 ) )
4 1 3 imbitrid ( 𝜒 → ( 𝜑𝜓 ) )