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
|- ( ph <-> ps )
biimtrid.2
|- ( ch -> ( ps -> th ) )
Assertion biimtrid
|- ( ch -> ( ph -> th ) )

Proof

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