Theorem bi13imp2

Description: Similar to 3imp except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017)

	Ref	Expression
Hypothesis	bi13imp2.1	|- ( ph <-> ( ps -> ( ch <-> th ) ) )
Assertion	bi13imp2	|- ( ( ph /\ ps /\ ch ) -> th )

Proof

Step	Hyp	Ref	Expression
1		bi13imp2.1	|- ( ph <-> ( ps -> ( ch <-> th ) ) )
2	1	biimpi	|- ( ph -> ( ps -> ( ch <-> th ) ) )
3	2	bi33imp12	|- ( ( ph /\ ps /\ ch ) -> th )