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	⊢ ( 𝜑 → 𝜓 )
	pm2.61iOLD.2	⊢ ( ¬ 𝜑 → 𝜓 )
Assertion	pm2.61iOLD	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		pm2.61iOLD.1	⊢ ( 𝜑 → 𝜓 )
2		pm2.61iOLD.2	⊢ ( ¬ 𝜑 → 𝜓 )
3		id	⊢ ( 𝜑 → 𝜑 )
4	2 1	ja	⊢ ( ( 𝜑 → 𝜑 ) → 𝜓 )
5	3 4	ax-mp	⊢ 𝜓