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

Theorem 3jaod 1420
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 1417 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1363 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1078
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 842  df-3or 1080  df-3an 1081
This theorem is referenced by:  3jaodan  1422  3jaao  1424  fntpb  6963  dfwe2  7485  smo11  7990  smoord  7991  omeulem1  8197  omopth2  8199  oaabs2  8261  elfiun  8882  r111  9192  r1pwss  9201  pwcfsdom  9993  winalim2  10106  xmullem  12645  xmulasslem  12666  xlemul1a  12669  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  ordtbas2  21727  ordtbas  21728  fmfnfmlem4  22493  dyadmbl  24128  scvxcvx  25490  perfectlem2  25733  2sq2  25936  ostth3  26141  satfun  32555  poseq  32992  sltsolem1  33077  lineext  33434  fscgr  33438  colinbtwnle  33476  broutsideof2  33480  lineunray  33505  lineelsb2  33506  elicc3  33562  4atlem11  36625  dalawlem10  36896  3cubeslem1  39159  frege129d  39986  goldbachth  43586  perfectALTVlem2  43764  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653
  Copyright terms: Public domain W3C validator