Theorem 3jaod 1338

Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem 3jaod

Step	Hyp	Ref	Expression
1		3jaod.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		3jaod.2	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
3		3jaod.3	. 2 ⊢ (𝜑 → (𝜏 → 𝜒))
4		3jao 1335	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1271	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))

Syntax hints:   → wi 4   ∨ w3o 1001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004

This theorem is referenced by:  3jaodan  1340  3jaao  1342  issod  4410  nnawordex  6683  exmidontri2or  7439  addlocprlem  7733  nqprloc  7743  ltexprlemrl  7808  aptiprleml  7837  aptiprlemu  7838  elnn0z  9470  zaddcl  9497  zletric  9501  zlelttric  9502  zltnle  9503  zdceq  9533  zdcle  9534  zdclt  9535  nn01to3  9824  xposdif  10090  fzdcel  10248  qletric  10473  qlelttric  10474  qltnle  10475  qdceq  10476  qdclt  10477  frec2uzlt2d  10638  perfectlem2  15689  triap  16457  tridceq  16484