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

Definition df-3or 974
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 524. (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 972 . 2
51, 2wo 368 . . 3
65, 3wo 368 . 2
74, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  3orass  976  3orrot  979  3anor  989  3ioran  991  3orbi123i  1186  3ori  1288  3jao  1289  mpjao3dan  1295  3orbi123d  1298  3orim123d  1307  3or6  1310  cadan  1459  nf3or  1936  eueq3  3274  sspsstri  3605  eltpg  4071  rextpg  4081  tppreqb  4171  somo  4839  ordtri1  4916  ordtri3  4919  ordeleqon  6624  bropopvvv  6880  soxp  6913  swoso  7361  en3lplem2  8053  cflim2  8664  entric  8953  entri2  8954  psslinpr  9430  ssxr  9675  relin01  10102  elznn0nn  10903  nn01to3  11204  xrnemnf  11357  xrnepnf  11358  xrsupss  11529  xrinfmss  11530  swrdnd  12657  cshwshashlem1  14580  tosso  15666  pmltpc  21862  dyaddisj  22005  legso  23985  colinearalg  24213  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  1to3vfriswmgra  25007  3o1cs  27369  3o2cs  27370  3o3cs  27371  tlt3  27653  3orel3  29089  3pm3.2ni  29090  3orit  29092  soseq  29334  nobnddown  29461  mblfinlem2  30052  ts3or1  30560  ts3or2  30561  ts3or3  30562  3orrabdioph  30717  sbc3or  33302  sbc3orgOLD  33303  en3lplem2VD  33644  3orbi123VD  33650  sbc3orgVD  33651
  Copyright terms: Public domain W3C validator