Metamath Proof Explorer


Theorem biimtrid

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993)

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

Proof

Step Hyp Ref Expression
1 biimtrid.1 ( 𝜑𝜓 )
2 biimtrid.2 ( 𝜒 → ( 𝜓𝜃 ) )
3 1 biimpi ( 𝜑𝜓 )
4 3 2 syl5 ( 𝜒 → ( 𝜑𝜃 ) )