Theorem pm2.61iOLD

Description: Obsolete version of pm2.61i as of 19-Nov-2023. (Contributed by NM, 5-Apr-1994) (Proof shortened by Wolf Lammen, 12-Sep-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pm2.61iOLD.1	$$⊢\phi \to \psi$$
	pm2.61iOLD.2	$$⊢\neg \phi \to \psi$$
Assertion	pm2.61iOLD	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.61iOLD.1	$$⊢\phi \to \psi$$
2		pm2.61iOLD.2	$$⊢\neg \phi \to \psi$$
3		id	$$⊢\phi \to \phi$$
4	2 1	ja	$$⊢\left(\phi \to \phi \right)\to \psi$$
5	3 4	ax-mp	$$⊢\psi$$