Theorem adh-minimp-ax2c

Description: Derivation of a commuted form of ax-2 from adh-minimp and ax-mp . Polish prefix notation: CCpqCCpCqrCpr . (Contributed by BJ, 4-Apr-2021) (Revised by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	adh-minimp-ax2c	⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		adh-minimp-jarr-ax2c-lem3	⊢ ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → 𝜑 )
2		adh-minimp-jarr-imim1-ax2c-lem1	⊢ ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → 𝜑 ) → ( ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) )
3	1 2	ax-mp	⊢ ( ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) )
4		adh-minimp-sylsimp	⊢ ( ( ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) )
5	3 4	ax-mp	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) )
6		adh-minimp-jarr-imim1-ax2c-lem1	⊢ ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) )
7	5 6	ax-mp	⊢ ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )
8		adh-minimp-sylsimp	⊢ ( ( ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) → ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) )
9	7 8	ax-mp	⊢ ( ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )
10		adh-minimp-jarr-imim1-ax2c-lem1	⊢ ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )
11		adh-minimp-imim1	⊢ ( ( ( 𝜑 → 𝜓 ) → ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) ) )
12	10 11	ax-mp	⊢ ( ( ( ( ( ( ( 𝜃 → 𝜏 ) → ( ( ( 𝜂 → 𝜃 ) → ( 𝜏 → 𝜁 ) ) → ( 𝜃 → 𝜁 ) ) ) → 𝜑 ) → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) ) )
13	9 12	ax-mp	⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) ) )