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

Theorem 3jaod 1432
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 1429 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1366 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1053
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 1055  df-3an 1056
This theorem is referenced by:  3jaodan  1434  3jaao  1436  fntpb  6514  dfwe2  7023  smo11  7506  smoord  7507  omeulem1  7707  omopth2  7709  oaabs2  7770  elfiun  8377  r111  8676  r1pwss  8685  pwcfsdom  9443  winalim2  9556  xmullem  12132  xmulasslem  12153  xlemul1a  12156  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  ordtbas2  21043  ordtbas  21044  fmfnfmlem4  21808  dyadmbl  23414  scvxcvx  24757  perfectlem2  25000  ostth3  25372  poseq  31878  sltsolem1  31951  lineext  32308  fscgr  32312  colinbtwnle  32350  broutsideof2  32354  lineunray  32379  lineelsb2  32380  elicc3  32436  4atlem11  35213  dalawlem10  35484  frege129d  38372  goldbachth  41784  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator