Theorem frege15

Description: A closed form of com4r . Proposition 15 of Frege1879 p. 38. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		frege12	$$⊢\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)\to \left(\left(\phi \to \left(\psi \to \left(\chi \to \left(\theta \to \tau \right)\right)\right)\right)\to \left(\theta \to \left(\phi \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(\theta \to \left(\phi \to \left(\psi \to \left(\chi \to \tau \right)\right)\right)\right)$$