Theorem 3jaodan 1457

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 417	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 417	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5		3jaodan.3	. . . 4 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
6	5	ex 417	. . 3 ⊢ (𝜑 → (𝜏 → 𝜒))
7	2, 4, 6	3jaod 1455	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
8	7	imp 411	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∨ w3o 1101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104

This theorem is used by:  mpjao3dan  1458  onzsl  7840  zeo  12688  xrltnsym  13168  xrlttri  13170  xrlttr  13171  qbtwnxr  13232  xltnegi  13248  xaddcom  13272  xnegdi  13280  xsubge0  13293  xrub  13344  bpoly3  16118  blssioo  24963  ismbf2d  25810  itg2seq  25912  eliccioo  33261  3ccased  36219  lineelsb2  36648  sticksstones1  42941  dfxlim2v  46589  usgrexmpl2trifr  48830