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

Theorem 3jaod 1425
 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 1422 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1368 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1083 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 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086 This theorem is referenced by:  3jaodan  1427  3jaao  1430  fntpb  6959  dfwe2  7489  smo11  8002  smoord  8003  omeulem1  8209  omopth2  8211  oaabs2  8273  elfiun  8896  r111  9206  r1pwss  9215  pwcfsdom  10012  winalim2  10125  xmullem  12665  xmulasslem  12686  xlemul1a  12689  xrsupsslem  12708  xrinfmsslem  12709  xrub  12713  symgvalstruct  18538  ordtbas2  21837  ordtbas  21838  fmfnfmlem4  22603  dyadmbl  24245  scvxcvx  25615  perfectlem2  25858  2sq2  26061  ostth3  26266  satfun  32837  poseq  33278  sltsolem1  33365  lineext  33797  fscgr  33801  colinbtwnle  33839  broutsideof2  33843  lineunray  33868  lineelsb2  33869  elicc3  33925  4atlem11  37056  dalawlem10  37327  3cubeslem1  39796  frege129d  40635  goldbachth  44232  perfectALTVlem2  44408  eenglngeehlnmlem1  45317  eenglngeehlnmlem2  45318
 Copyright terms: Public domain W3C validator