This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem jaoded

Description: Deduction form of jao . Disjunction of antecedents. (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		jaoded.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		jaoded.2	⊢ ( 𝜃 → ( 𝜏 → 𝜒 ) )
3		jaoded.3	⊢ ( 𝜂 → ( 𝜓 ∨ 𝜏 ) )
4		jao	⊢ ( ( 𝜓 → 𝜒 ) → ( ( 𝜏 → 𝜒 ) → ( ( 𝜓 ∨ 𝜏 ) → 𝜒 ) ) )
5	4	3imp	⊢ ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜏 → 𝜒 ) ∧ ( 𝜓 ∨ 𝜏 ) ) → 𝜒 )
6	1 2 3 5	syl3an	⊢ ( ( 𝜑 ∧ 𝜃 ∧ 𝜂 ) → 𝜒 )