Theorem 3jaod 1431

Description: Disjunction of three 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 1427	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))

Syntax hints:   → wi 4   ∨ w3o 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaodan  1433  3jaao  1435  fntpb  7143  dfwe2  7707  poseq  8088  smo11  8284  smoord  8285  omeulem1  8497  omopth2  8499  oaabs2  8564  elfiun  9314  r111  9668  r1pwss  9677  pwcfsdom  10474  winalim2  10587  xmullem  13163  xmulasslem  13184  xlemul1a  13187  xrsupsslem  13206  xrinfmsslem  13207  xrub  13211  fvf1tp  13693  symgvalstruct  19309  ordtbas2  23106  ordtbas  23107  fmfnfmlem4  23872  dyadmbl  25528  scvxcvx  26923  perfectlem2  27168  2sq2  27371  ostth3  27576  sltsolem1  27614  addsproplem7  27918  negsproplem7  27976  mulsproplem5  28059  mulsproplem6  28060  mulsproplem7  28061  mulsproplem8  28062  satfun  35455  lineext  36120  fscgr  36124  colinbtwnle  36162  broutsideof2  36166  lineunray  36191  lineelsb2  36192  elicc3  36361  4atlem11  39718  dalawlem10  39989  3cubeslem1  42787  dflim5  43432  omabs2  43435  omcl3g  43437  naddwordnexlem4  43504  frege129d  43866  goldbachth  47657  perfectALTVlem2  47832  gpgiedgdmellem  48156  gpgusgralem  48166  gpgvtxedg0  48173  gpgvtxedg1  48174  gpgedgiov  48175  gpgedg2ov  48176  gpgedg2iv  48177  gpgnbgrvtx0  48184  gpgnbgrvtx1  48185  pgnioedg1  48218  pgnioedg2  48219  pgnioedg3  48220  pgnioedg4  48221  pgnioedg5  48222  pgnbgreunbgrlem1  48223  pgnbgreunbgrlem2  48227  pgnbgreunbgrlem4  48229  pgnbgreunbgrlem5lem1  48230  pgnbgreunbgrlem5lem2  48231  pgnbgreunbgrlem5lem3  48232  pgnbgreunbgrlem5  48233  eenglngeehlnmlem1  48848  eenglngeehlnmlem2  48849