Theorem frege14

Description: Closed form of a deduction based on com3r . Proposition 14 of Frege1879 p. 37. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege14	$$⊢\left(\phi \to \left(\psi \to \left(\chi \to \left(\theta \to \tau \right)\right)\right)\right)\to \left(\phi \to \left(\theta \to \left(\psi \to \left(\chi \to \tau \right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege13	$$⊢\left(\psi \to \left(\chi \to \left(\theta \to \tau \right)\right)\right)\to \left(\theta \to \left(\psi \to \left(\chi \to \tau \right)\right)\right)$$
2		frege5	$$⊢\left(\left(\psi \to \left(\chi \to \left(\theta \to \tau \right)\right)\right)\to \left(\theta \to \left(\psi \to \left(\chi \to \tau \right)\right)\right)\right)\to \left(\left(\phi \to \left(\psi \to \left(\chi \to \left(\theta \to \tau \right)\right)\right)\right)\to \left(\phi \to \left(\theta \to \left(\psi \to \left(\chi \to \tau \right)\right)\right)\right)\right)$$
3	1 2	ax-mp	$$⊢\left(\phi \to \left(\psi \to \left(\chi \to \left(\theta \to \tau \right)\right)\right)\right)\to \left(\phi \to \left(\theta \to \left(\psi \to \left(\chi \to \tau \right)\right)\right)\right)$$