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  6696  exmidontri2or  7460  addlocprlem  7754  nqprloc  7764  ltexprlemrl  7829  aptiprleml  7858  aptiprlemu  7859  elnn0z  9491  zaddcl  9518  zletric  9522  zlelttric  9523  zltnle  9524  zdceq  9554  zdcle  9555  zdclt  9556  nn01to3  9850  xposdif  10116  fzdcel  10274  qletric  10500  qlelttric  10501  qltnle  10502  qdceq  10503  qdclt  10504  frec2uzlt2d  10665  perfectlem2  15723  triap  16633  tridceq  16660