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	|- ( ( ph /\ ps ) -> ch )
	mpjao3dan.2	|- ( ( ph /\ th ) -> ch )
	mpjao3dan.3	|- ( ( ph /\ ta ) -> ch )
	mpjao3dan.4	|- ( ph -> ( ps \/ th \/ ta ) )
Assertion	mpjao3danOLD	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		mpjao3dan.1	|- ( ( ph /\ ps ) -> ch )
2		mpjao3dan.2	|- ( ( ph /\ th ) -> ch )
3		mpjao3dan.3	|- ( ( ph /\ ta ) -> ch )
4		mpjao3dan.4	|- ( ph -> ( ps \/ th \/ ta ) )
5	1 2	jaodan	|- ( ( ph /\ ( ps \/ th ) ) -> ch )
6		df-3or	|- ( ( ps \/ th \/ ta ) <-> ( ( ps \/ th ) \/ ta ) )
7	4 6	sylib	|- ( ph -> ( ( ps \/ th ) \/ ta ) )
8	5 3 7	mpjaodan	|- ( ph -> ch )