Theorem 3jaod 1340

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

Syntax hints:   → wi 4   ∨ w3o 1003

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 716

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

This theorem is referenced by:  3jaodan  1342  3jaao  1344  issod  4416  nnawordex  6697  exmidontri2or  7461  addlocprlem  7755  nqprloc  7765  ltexprlemrl  7830  aptiprleml  7859  aptiprlemu  7860  elnn0z  9492  zaddcl  9519  zletric  9523  zlelttric  9524  zltnle  9525  zdceq  9555  zdcle  9556  zdclt  9557  nn01to3  9851  xposdif  10117  fzdcel  10275  qletric  10502  qlelttric  10503  qltnle  10504  qdceq  10505  qdclt  10506  frec2uzlt2d  10667  perfectlem2  15730  triap  16659  tridceq  16687