Theorem frege22

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

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

Proof

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