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

Definition df-or 359
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 20824). After we define the constant true  T. (df-tru 1310) and the constant false  F. (df-fal 1311), we will be able to prove these truth table values:  ( (  T.  \/  T.  )  <->  T.  ) (truortru 1330), 
( (  T.  \/  F.  )  <->  T.  ) (truorfal 1331), 
( (  F.  \/  T.  )  <->  T.  ) (falortru 1332), and  ( (  F.  \/  F.  )  <->  F.  ) (falorfal 1333).

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 227. This is the justification for the definition, along with the fact that it introduces a new symbol  \/. Contrast with  /\ (df-an 360), 
-> (wi 4),  -/\ (df-nan 1288), and  \/_ (df-xor 1296) . (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 357 . 2  wff  ( ph  \/  ps )
41wn 3 . . 3  wff  -.  ph
54, 2wi 4 . 2  wff  ( -. 
ph  ->  ps )
63, 5wb 176 1  wff  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
Colors of variables: wff set class
This definition is referenced by:  pm4.64  361  pm2.53  362  pm2.54  363  ori  364  orri  365  ord  366  imor  401  mtord  641  orbi2d  682  orimdi  820  ordi  834  pm5.17  858  pm5.6  878  orbidi  898  cador  1381  cadan  1382  19.30  1594  19.43  1595  nfor  1782  19.32  1823  dfsb3  2009  sbor  2019  neor  2543  r19.30  2698  r19.32v  2699  r19.43  2708  dfif2  3580  disjor  4023  sotric  4356  sotrieq  4357  isso2i  4362  soxp  6244  unxpwdom2  7318  cflim2  7905  cfpwsdom  8222  ltapr  8685  ltxrlt  8909  isprm4  12784  euclemma  12803  islpi  16896  restntr  16928  alexsubALTlem2  17758  alexsubALTlem3  17759  2bornot2b  20853  ballotlemodife  23072  funcnv5mpt  23251  disjorf  23371  3orit  24081  dfon2lem5  24214  nxtor  25088  ecase13d  26325  elicc3  26331  nn0prpw  26342  pm10.541  27665  fmul01lt1lem1  27817  stoweidlem34  27886  stoweidlem35  27887  r19.32  28048  sborNEW7  29541  dfsb3NEW7  29610
  Copyright terms: Public domain W3C validator