Theorem mpjao3danOLD

Description: Obsolete version of mpjao3dan as of 17-Apr-2024. (Contributed by Thierry Arnoux, 13-Apr-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	mpjao3dan.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
	mpjao3dan.2	⊢ ( ( 𝜑 ∧ 𝜃 ) → 𝜒 )
	mpjao3dan.3	⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜒 )
	mpjao3dan.4	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜃 ∨ 𝜏 ) )
Assertion	mpjao3danOLD	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		mpjao3dan.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2		mpjao3dan.2	⊢ ( ( 𝜑 ∧ 𝜃 ) → 𝜒 )
3		mpjao3dan.3	⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜒 )
4		mpjao3dan.4	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜃 ∨ 𝜏 ) )
5	1 2	jaodan	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜃 ) ) → 𝜒 )
6		df-3or	⊢ ( ( 𝜓 ∨ 𝜃 ∨ 𝜏 ) ↔ ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜏 ) )
7	4 6	sylib	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜏 ) )
8	5 3 7	mpjaodan	⊢ ( 𝜑 → 𝜒 )