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

Theorem 3jaod 1389
 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 1386 . 2 (((𝜓𝜒) ∧ (𝜃𝜒) ∧ (𝜏𝜒)) → ((𝜓𝜃𝜏) → 𝜒))
51, 2, 3, 4syl3anc 1323 1 (𝜑 → ((𝜓𝜃𝜏) → 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1035 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 385  df-an 386  df-3or 1037  df-3an 1038 This theorem is referenced by:  3jaodan  1391  3jaao  1393  fntpb  6427  dfwe2  6928  smo11  7406  smoord  7407  omeulem1  7607  omopth2  7609  oaabs2  7670  elfiun  8280  r111  8582  r1pwss  8591  pwcfsdom  9349  winalim2  9462  xmullem  12037  xmulasslem  12058  xlemul1a  12061  xrsupsslem  12080  xrinfmsslem  12081  xrub  12085  ordtbas2  20905  ordtbas  20906  fmfnfmlem4  21671  dyadmbl  23274  scvxcvx  24612  perfectlem2  24855  ostth3  25227  poseq  31451  sltsolem1  31528  lineext  31825  fscgr  31829  colinbtwnle  31867  broutsideof2  31871  lineunray  31896  lineelsb2  31897  elicc3  31953  4atlem11  34375  dalawlem10  34646  frege129d  37536  goldbachth  40758  perfectALTVlem2  40926
 Copyright terms: Public domain W3C validator