Theorem orim12da

Description: Deduce a disjunction from another one. Variation on orim12d . (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	orim12da.1	|- ( ( ph /\ ps ) -> th )
	orim12da.2	|- ( ( ph /\ ch ) -> ta )
	orim12da.3	|- ( ph -> ( ps \/ ch ) )
Assertion	orim12da	|- ( ph -> ( th \/ ta ) )

Proof

Step	Hyp	Ref	Expression
1		orim12da.1	|- ( ( ph /\ ps ) -> th )
2		orim12da.2	|- ( ( ph /\ ch ) -> ta )
3		orim12da.3	|- ( ph -> ( ps \/ ch ) )
4	1	ex	|- ( ph -> ( ps -> th ) )
5	2	ex	|- ( ph -> ( ch -> ta ) )
6	4 5	orim12d	|- ( ph -> ( ( ps \/ ch ) -> ( th \/ ta ) ) )
7	3 6	mpd	|- ( ph -> ( th \/ ta ) )