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

Definition df-or 361
Description: Define disjunction (logical 'or'). Definition of [Margaris] p. 49. When the left operand, right operand, or both are true, the result is true; when both sides are false, the result is false. For example, it is true that  ( 2  =  3  \/  4  =  4 ) (ex-or 20784). After we define the constant true  T. (df-tru 1312) and the constant false  F. (df-fal 1313), we will be able to prove these truth table values:  ( (  T.  \/  T.  )  <->  T.  ) (truortru 1332), 
( (  T.  \/  F.  )  <->  T.  ) (truorfal 1333), 
( (  F.  \/  T.  )  <->  T.  ) (falortru 1334), and  ( (  F.  \/  F.  )  <->  F.  ) (falorfal 1335).

This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute  ( -.  ph  ->  ps ) for  ( ph  \/  ps ), we end up with an instance of previously proved theorem biid 229. This is the justification for the definition, along with the fact that it introduces a new symbol  \/. Contrast with  /\ (df-an 362), 
-> (wi 6),  -/\ (df-nan 1290), and  \/_ (df-xor 1298) . (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
df-or  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wo 359 . 2  wff  ( ph  \/  ps )
41wn 5 . . 3  wff  -.  ph
54, 2wi 6 . 2  wff  ( -. 
ph  ->  ps )
63, 5wb 178 1  wff  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
Colors of variables: wff set class
This definition is referenced by:  pm4.64  363  pm2.53  364  pm2.54  365  ori  366  orri  367  ord  368  imor  403  mtord  643  orbi2d  684  orimdi  822  ordi  836  pm5.17  860  pm5.6  880  orbidi  900  cador  1383  cadan  1384  19.30  1592  19.43  1593  nfor  1772  19.32  1813  dfsb3  1996  sbor  2006  neor  2532  r19.30  2687  r19.32v  2688  r19.43  2697  dfif2  3569  disjor  4009  sotric  4340  sotrieq  4341  isso2i  4346  soxp  6190  unxpwdom2  7298  cflim2  7885  cfpwsdom  8202  ltapr  8665  ltxrlt  8889  isprm4  12763  euclemma  12782  islpi  16875  restntr  16907  alexsubALTlem2  17737  alexsubALTlem3  17738  2bornot2b  20830  ballotlemodife  23050  3orit  23471  dfon2lem5  23545  nxtor  24384  ecase13d  25622  elicc3  25628  nn0prpw  25639  pm10.541  26962  fmul01lt1lem1  27114  stoweidlem34  27183  stoweidlem35  27184  r19.32  27325
  Copyright terms: Public domain W3C validator