Theorem 3orim123d

Description: Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997)

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

Proof

Step	Hyp	Ref	Expression
1		3anim123d.1	|- ( ph -> ( ps -> ch ) )
2		3anim123d.2	|- ( ph -> ( th -> ta ) )
3		3anim123d.3	|- ( ph -> ( et -> ze ) )
4	1 2	orim12d	|- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )
5	4 3	orim12d	|- ( ph -> ( ( ( ps \/ th ) \/ et ) -> ( ( ch \/ ta ) \/ ze ) ) )
6		df-3or	|- ( ( ps \/ th \/ et ) <-> ( ( ps \/ th ) \/ et ) )
7		df-3or	|- ( ( ch \/ ta \/ ze ) <-> ( ( ch \/ ta ) \/ ze ) )
8	5 6 7	3imtr4g	|- ( ph -> ( ( ps \/ th \/ et ) -> ( ch \/ ta \/ ze ) ) )