Theorem frege34

Description: If as a conseqence of the occurrence of the circumstance ph , when the obstacle ps is removed, ch takes place, then from the circumstance that ch does not take place while ph occurs the occurrence of the obstacle ps can be inferred. Closed form of con1d . Proposition 34 of Frege1879 p. 45. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege34	$$⊢\left(\phi \to \left(\neg \psi \to \chi \right)\right)\to \left(\phi \to \left(\neg \chi \to \psi \right)\right)$$

Proof

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