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  7155  dfwe2  7719  poseq  8100  smo11  8296  smoord  8297  omeulem1  8509  omopth2  8511  oaabs2  8577  elfiun  9333  r111  9687  r1pwss  9696  pwcfsdom  10494  winalim2  10607  xmullem  13179  xmulasslem  13200  xlemul1a  13203  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  fvf1tp  13709  symgvalstruct  19326  ordtbas2  23135  ordtbas  23136  fmfnfmlem4  23901  dyadmbl  25557  scvxcvx  26952  perfectlem2  27197  2sq2  27400  ostth3  27605  ltssolem1  27643  addsproplem7  27971  negsproplem7  28030  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  satfun  35605  lineext  36270  fscgr  36274  colinbtwnle  36312  broutsideof2  36316  lineunray  36341  lineelsb2  36342  elicc3  36511  4atlem11  39869  dalawlem10  40140  3cubeslem1  42926  dflim5  43571  omabs2  43574  omcl3g  43576  naddwordnexlem4  43643  frege129d  44004  goldbachth  47793  perfectALTVlem2  47968  gpgiedgdmellem  48292  gpgusgralem  48302  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedgiov  48311  gpgedg2ov  48312  gpgedg2iv  48313  gpgnbgrvtx0  48320  gpgnbgrvtx1  48321  pgnioedg1  48354  pgnioedg2  48355  pgnioedg3  48356  pgnioedg4  48357  pgnioedg5  48358  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  pgnbgreunbgrlem5  48369  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984