Metamath Proof Explorer


Theorem ibd

Description: Deduction that converts a biconditional implied by one of its arguments, into an implication. Deduction associated with ibi . (Contributed by NM, 26-Jun-2004)

Ref Expression
Hypothesis ibd.1 ( 𝜑 → ( 𝜓 → ( 𝜓𝜒 ) ) )
Assertion ibd ( 𝜑 → ( 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 ibd.1 ( 𝜑 → ( 𝜓 → ( 𝜓𝜒 ) ) )
2 biimp ( ( 𝜓𝜒 ) → ( 𝜓𝜒 ) )
3 1 2 syli ( 𝜑 → ( 𝜓𝜒 ) )