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 20621). After we define the constant true  T. (df-tru 1315) and the constant false  F. (df-fal 1316), we will be able to prove these truth table values:  ( (  T.  \/  T.  )  <->  T.  ) (truortru 1336), 
( (  T.  \/  F.  )  <->  T.  ) (truorfal 1337), 
( (  F.  \/  T.  )  <->  T.  ) (falortru 1338), and  ( (  F.  \/  F.  )  <->  F.  ) (falorfal 1339).

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 1293), and  \/_ (df-xor 1301) . (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  644  orbi2d  685  orimdi  823  ordi  837  pm5.17  863  pm5.6  883  orbidi  903  cador  1387  cadan  1388  19.30  1603  19.43  1604  nfor  1736  19.32  1794  dfsb3  1948  sbor  1958  neor  2496  r19.30  2647  r19.32v  2648  r19.43  2657  dfif2  3472  disjor  3904  sotric  4233  sotrieq  4234  isso2i  4239  soxp  6080  unxpwdom2  7186  cflim2  7773  cfpwsdom  8086  ltapr  8549  ltxrlt  8773  isprm4  12642  euclemma  12661  islpi  16712  restntr  16744  alexsubALTlem2  17574  alexsubALTlem3  17575  2bornot2b  20667  3orit  23237  dfon2lem5  23311  nxtor  24150  ecase13d  25388  elicc3  25394  nn0prpw  25405  pm10.541  26728  fmul01lt1lem1  26881  stoweidlem34  26917  stoweidlem35  26918
  Copyright terms: Public domain W3C validator