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  7822  zeo  12620  xrltnsym  13097  xrlttri  13099  xrlttr  13100  qbtwnxr  13160  xltnegi  13176  xaddcom  13200  xnegdi  13208  xsubge0  13221  xrub  13272  bpoly3  16024  blssioo  24683  ismbf2d  25541  itg2seq  25643  eliccioo  32851  3ccased  35706  lineelsb2  36136  sticksstones1  42134  dfxlim2v  45845  usgrexmpl2trifr  48028