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

Theorem 3jaod 1541
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 1537 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1477 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1071
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 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074
This theorem is referenced by:  3jaodan  1543  3jaao  1545  fntpb  6638  dfwe2  7147  smo11  7631  smoord  7632  omeulem1  7833  omopth2  7835  oaabs2  7896  elfiun  8503  r111  8813  r1pwss  8822  pwcfsdom  9617  winalim2  9730  xmullem  12307  xmulasslem  12328  xlemul1a  12331  xrsupsslem  12350  xrinfmsslem  12351  xrub  12355  ordtbas2  21217  ordtbas  21218  fmfnfmlem4  21982  dyadmbl  23588  scvxcvx  24932  perfectlem2  25175  ostth3  25547  poseq  32080  sltsolem1  32153  lineext  32510  fscgr  32514  colinbtwnle  32552  broutsideof2  32556  lineunray  32581  lineelsb2  32582  elicc3  32638  4atlem11  35416  dalawlem10  35687  frege129d  38575  goldbachth  41987  perfectALTVlem2  42159
  Copyright terms: Public domain W3C validator