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  7186  dfwe2  7753  poseq  8140  smo11  8336  smoord  8337  omeulem1  8549  omopth2  8551  oaabs2  8616  elfiun  9388  r111  9735  r1pwss  9744  pwcfsdom  10543  winalim2  10656  xmullem  13231  xmulasslem  13252  xlemul1a  13255  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  fvf1tp  13758  symgvalstruct  19334  ordtbas2  23085  ordtbas  23086  fmfnfmlem4  23851  dyadmbl  25508  scvxcvx  26903  perfectlem2  27148  2sq2  27351  ostth3  27556  sltsolem1  27594  addsproplem7  27889  negsproplem7  27947  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  satfun  35405  lineext  36071  fscgr  36075  colinbtwnle  36113  broutsideof2  36117  lineunray  36142  lineelsb2  36143  elicc3  36312  4atlem11  39610  dalawlem10  39881  3cubeslem1  42679  dflim5  43325  omabs2  43328  omcl3g  43330  naddwordnexlem4  43397  frege129d  43759  goldbachth  47552  perfectALTVlem2  47727  gpgiedgdmellem  48041  gpgusgralem  48051  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgrlem5  48117  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731