MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3or Unicode version

Definition df-3or 951
Description: Define disjunction ('or') of three wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 514. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3or

Detailed syntax breakdown of Definition df-3or
StepHypRef Expression
1 wph . . 3
2 wps . . 3
3 wch . . 3
41, 2, 3w3o 949 . 2
51, 2wo 361 . . 3
65, 3wo 361 . 2
74, 6wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  3orass  953  3orrot  956  3anor  966  3ioran  968  3orbi123i  1162  3ori  1263  3jao  1264  mpjao3dan  1270  3orbi123d  1273  3orim123d  1282  3or6  1285  cadan  1427  cadanOLD  1428  nf3or  1859  eueq3  3112  sspsstri  3435  eltpg  3895  rextpg  3905  tppreqb  3989  somo  4646  ordtri1  4723  ordtri3  4726  ordeleqon  6370  bropopvvv  6622  soxp  6654  swoso  7093  en3lplem2  7768  cflim2  8379  entric  8668  entri2  8669  psslinpr  9146  ssxr  9390  relin01  9810  nnnegz  10594  elznn0nn  10605  xrnemnf  11044  xrnepnf  11045  xrsupss  11216  xrinfmss  11217  swrdnd  12267  cshwshashlem1  14062  tosso  15146  pmltpc  20634  dyaddisj  20776  colinearalg  22835  3o1cs  25533  3o2cs  25534  3o3cs  25535  tlt3  25804  3orel3  27070  3pm3.2ni  27071  3orit  27073  soseq  27417  nobnddown  27544  mblfinlem2  28100  ts3or1  28635  ts3or2  28636  ts3or3  28637  3orrabdioph  28795  nn01to3  29861  2wlkonot3v  30068  2spthonot3v  30069  clwwlknprop  30109  1to3vfriswmgra  30273  sbc3or  30814  sbc3orgOLD  30815  en3lplem2VD  31158  3orbi123VD  31164  sbc3orgVD  31165
  Copyright terms: Public domain W3C validator