Metamath Proof Explorer


Theorem imbitrdi

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypotheses imbitrdi.1
|- ( ph -> ( ps -> ch ) )
imbitrdi.2
|- ( ch <-> th )
Assertion imbitrdi
|- ( ph -> ( ps -> th ) )

Proof

Step Hyp Ref Expression
1 imbitrdi.1
 |-  ( ph -> ( ps -> ch ) )
2 imbitrdi.2
 |-  ( ch <-> th )
3 2 biimpi
 |-  ( ch -> th )
4 1 3 syl6
 |-  ( ph -> ( ps -> th ) )