Theorem 3jaodan 1434

Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
3jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3jaodan.3	⊢ ((𝜑 ∧ 𝜏) → 𝜒)

Assertion

Ref	Expression
3jaodan	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)

Proof of Theorem 3jaodan

Step	Hyp	Ref	Expression
1		3jaodan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 412	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5		3jaodan.3	. . . 4 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
6	5	ex 412	. . 3 ⊢ (𝜑 → (𝜏 → 𝜒))
7	2, 4, 6	3jaod 1432	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
8	7	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  mpjao3dan  1435  onzsl  7797  zeo  12615  xrltnsym  13088  xrlttri  13090  xrlttr  13091  qbtwnxr  13152  xltnegi  13168  xaddcom  13192  xnegdi  13200  xsubge0  13213  xrub  13264  bpoly3  16023  blssioo  24760  ismbf2d  25607  itg2seq  25709  eliccioo  32990  3ccased  35901  lineelsb2  36330  sticksstones1  42585  dfxlim2v  46275  usgrexmpl2trifr  48513