MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3jaod Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3jaod.1 . 2 (𝜑 → (𝜓𝜒))
2 3jaod.2 . 2 (𝜑 → (𝜃𝜒))
3 3jaod.3 . 2 (𝜑 → (𝜏𝜒))
4 3jao 1427 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1373 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1086
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 849  df-3or 1088  df-3an 1089
This theorem is referenced by:  3jaodan  1433  3jaao  1435  fntpb  7229  dfwe2  7794  poseq  8183  smo11  8404  smoord  8405  omeulem1  8620  omopth2  8622  oaabs2  8687  elfiun  9470  r111  9815  r1pwss  9824  pwcfsdom  10623  winalim2  10736  xmullem  13306  xmulasslem  13327  xlemul1a  13330  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  fvf1tp  13829  symgvalstruct  19414  symgvalstructOLD  19415  ordtbas2  23199  ordtbas  23200  fmfnfmlem4  23965  dyadmbl  25635  scvxcvx  27029  perfectlem2  27274  2sq2  27477  ostth3  27682  sltsolem1  27720  addsproplem7  28008  negsproplem7  28066  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  satfun  35416  lineext  36077  fscgr  36081  colinbtwnle  36119  broutsideof2  36123  lineunray  36148  lineelsb2  36149  elicc3  36318  4atlem11  39611  dalawlem10  39882  3cubeslem1  42695  dflim5  43342  omabs2  43345  omcl3g  43347  naddwordnexlem4  43414  frege129d  43776  goldbachth  47534  perfectALTVlem2  47709  gpgedgel  48007  gpgusgralem  48011  gpgvtxedg0  48021  gpgvtxedg1  48022  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659
  Copyright terms: Public domain W3C validator