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

Theorem 3jaod 1546
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 1542 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1483 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1099
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 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102
This theorem is referenced by:  3jaodan  1548  3jaao  1550  fntpb  6694  dfwe2  7207  smo11  7693  smoord  7694  omeulem1  7895  omopth2  7897  oaabs2  7958  elfiun  8571  r111  8881  r1pwss  8890  pwcfsdom  9686  winalim2  9799  xmullem  12308  xmulasslem  12329  xlemul1a  12332  xrsupsslem  12351  xrinfmsslem  12352  xrub  12356  ordtbas2  21205  ordtbas  21206  fmfnfmlem4  21970  dyadmbl  23577  scvxcvx  24922  perfectlem2  25165  ostth3  25537  poseq  32069  sltsolem1  32142  lineext  32499  fscgr  32503  colinbtwnle  32541  broutsideof2  32545  lineunray  32570  lineelsb2  32571  elicc3  32627  4atlem11  35384  dalawlem10  35655  frege129d  38549  goldbachth  42028  perfectALTVlem2  42200
  Copyright terms: Public domain W3C validator