Metamath Proof Explorer

Theorem imbi13

Description: Join three logical equivalences to form equivalence of implications. imbi13 is imbi13VD without virtual deductions and was automatically derived from imbi13VD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	imbi13	\|- ( ( ph <-> ps ) -> ( ( ch <-> th ) -> ( ( ta <-> et ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th -> et ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		imbi12	\|- ( ( ch <-> th ) -> ( ( ta <-> et ) -> ( ( ch -> ta ) <-> ( th -> et ) ) ) )
2		imbi12	\|- ( ( ph <-> ps ) -> ( ( ( ch -> ta ) <-> ( th -> et ) ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th -> et ) ) ) ) )
3	1 2	syl9r	\|- ( ( ph <-> ps ) -> ( ( ch <-> th ) -> ( ( ta <-> et ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th -> et ) ) ) ) ) )

Step

Hyp

Ref

Expression

imbi12

 |-  ( ( ch <-> th ) -> ( ( ta <-> et ) -> ( ( ch -> ta ) <-> ( th -> et ) ) ) )

imbi12

 |-  ( ( ph <-> ps ) -> ( ( ( ch -> ta ) <-> ( th -> et ) ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th -> et ) ) ) ) )

1 2

syl9r

 |-  ( ( ph <-> ps ) -> ( ( ch <-> th ) -> ( ( ta <-> et ) -> ( ( ph -> ( ch -> ta ) ) <-> ( ps -> ( th -> et ) ) ) ) ) )