Theorem 3jaoi 1344

Description: Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)

Hypotheses

Ref	Expression
3jaoi.1	⊢ (𝜑 → 𝜓)
3jaoi.2	⊢ (𝜒 → 𝜓)
3jaoi.3	⊢ (𝜃 → 𝜓)

Assertion

Ref	Expression
3jaoi	⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Proof of Theorem 3jaoi

Step	Hyp	Ref	Expression
1		3jaoi.1	. . 3 ⊢ (𝜑 → 𝜓)
2		3jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3		3jaoi.3	. . 3 ⊢ (𝜃 → 𝜓)
4	1, 2, 3	3pm3.2i 1206	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1342	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
6	4, 5	ax-mp 5	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1008   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011

This theorem is used by:  3jaoian  1346  3ianorr  1350  acexmidlem1  6084  nndceq  6776  nndcel  6777  znegcl  9686  xrltnr  10198  nltpnft  10233  ngtmnft  10236  xrrebnd  10238  xnegcl  10251  xnegneg  10252  xltnegi  10254  xrpnfdc  10261  xrmnfdc  10262  xnegid  10278  xaddid1  10281  xposdif  10301  prm23lt5  13071  ppiublem1  16291  zabsle1  16323  gausslemma2dlem0f  16378  gausslemma2dlem0i  16381  2lgsoddprm  16437