Theorem orel

Description: An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019)

	Ref	Expression
Hypotheses	orel.1	⊢ ( ( 𝜓 ∧ 𝜂 ) → 𝜃 )
	orel.2	⊢ ( ( 𝜒 ∧ 𝜌 ) → 𝜃 )
	orel.3	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
Assertion	orel	⊢ ( ( 𝜑 ∧ ( 𝜂 ∧ 𝜌 ) ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		orel.1	⊢ ( ( 𝜓 ∧ 𝜂 ) → 𝜃 )
2		orel.2	⊢ ( ( 𝜒 ∧ 𝜌 ) → 𝜃 )
3		orel.3	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) )
4		simprl	⊢ ( ( 𝜑 ∧ ( 𝜂 ∧ 𝜌 ) ) → 𝜂 )
5	1	ancoms	⊢ ( ( 𝜂 ∧ 𝜓 ) → 𝜃 )
6	4 5	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝜂 ∧ 𝜌 ) ) ∧ 𝜓 ) → 𝜃 )
7		simprr	⊢ ( ( 𝜑 ∧ ( 𝜂 ∧ 𝜌 ) ) → 𝜌 )
8	2	ancoms	⊢ ( ( 𝜌 ∧ 𝜒 ) → 𝜃 )
9	7 8	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝜂 ∧ 𝜌 ) ) ∧ 𝜒 ) → 𝜃 )
10	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝜂 ∧ 𝜌 ) ) → ( 𝜓 ∨ 𝜒 ) )
11	6 9 10	mpjaodan	⊢ ( ( 𝜑 ∧ ( 𝜂 ∧ 𝜌 ) ) → 𝜃 )