Theorem 3jaodan 1433

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 1431	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
8	7	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)

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

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 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  mpjao3dan  1434  onzsl  7802  zeo  12596  xrltnsym  13073  xrlttri  13075  xrlttr  13076  qbtwnxr  13136  xltnegi  13152  xaddcom  13176  xnegdi  13184  xsubge0  13197  xrub  13248  bpoly3  16000  blssioo  24716  ismbf2d  25574  itg2seq  25676  eliccioo  32901  3ccased  35699  lineelsb2  36129  sticksstones1  42127  dfxlim2v  45838  usgrexmpl2trifr  48021