Theorem 3jaod 1341

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

Syntax hints:   → wi 4   ∨ w3o 1004

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 717

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007

This theorem is referenced by:  3jaodan  1343  3jaao  1345  issod  4422  nnawordex  6740  exmidontri2or  7504  addlocprlem  7798  nqprloc  7808  ltexprlemrl  7873  aptiprleml  7902  aptiprlemu  7903  elnn0z  9536  zaddcl  9563  zletric  9567  zlelttric  9568  zltnle  9569  zdceq  9599  zdcle  9600  zdclt  9601  nn01to3  9895  xposdif  10161  fzdcel  10320  qletric  10547  qlelttric  10548  qltnle  10549  qdceq  10550  qdclt  10551  frec2uzlt2d  10712  perfectlem2  15797  triap  16744  tridceq  16772