Theorem frege23

Description: Syllogism followed by rotation of three antecedents. Proposition 23 of Frege1879 p. 42. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

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