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  7779  zeo  12562  xrltnsym  13039  xrlttri  13041  xrlttr  13042  qbtwnxr  13102  xltnegi  13118  xaddcom  13142  xnegdi  13150  xsubge0  13163  xrub  13214  bpoly3  15965  blssioo  24681  ismbf2d  25539  itg2seq  25641  eliccioo  32880  3ccased  35712  lineelsb2  36142  sticksstones1  42139  dfxlim2v  45848  usgrexmpl2trifr  48041