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

Theorem 3jaod 1422
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 1419 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1365 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1080
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 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083
This theorem is referenced by:  3jaodan  1424  3jaao  1426  fntpb  6970  dfwe2  7487  smo11  7995  smoord  7996  omeulem1  8201  omopth2  8203  oaabs2  8265  elfiun  8886  r111  9196  r1pwss  9205  pwcfsdom  9997  winalim2  10110  xmullem  12650  xmulasslem  12671  xlemul1a  12674  xrsupsslem  12693  xrinfmsslem  12694  xrub  12698  ordtbas2  21717  ordtbas  21718  fmfnfmlem4  22483  dyadmbl  24118  scvxcvx  25479  perfectlem2  25722  2sq2  25925  ostth3  26130  satfun  32544  poseq  32981  sltsolem1  33066  lineext  33423  fscgr  33427  colinbtwnle  33465  broutsideof2  33469  lineunray  33494  lineelsb2  33495  elicc3  33551  4atlem11  36614  dalawlem10  36885  3cubeslem1  39148  frege129d  39975  goldbachth  43543  perfectALTVlem2  43721  eenglngeehlnmlem1  44558  eenglngeehlnmlem2  44559
  Copyright terms: Public domain W3C validator