Theorem 3jaod 1317

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 1314	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1250	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))

Syntax hints:   → wi 4   ∨ w3o 980

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 711

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983

This theorem is referenced by:  3jaodan  1319  3jaao  1321  issod  4366  nnawordex  6615  exmidontri2or  7355  addlocprlem  7648  nqprloc  7658  ltexprlemrl  7723  aptiprleml  7752  aptiprlemu  7753  elnn0z  9385  zaddcl  9412  zletric  9416  zlelttric  9417  zltnle  9418  zdceq  9448  zdcle  9449  zdclt  9450  nn01to3  9738  xposdif  10004  fzdcel  10162  qletric  10384  qlelttric  10385  qltnle  10386  qdceq  10387  qdclt  10388  frec2uzlt2d  10549  perfectlem2  15472  triap  15968  tridceq  15995