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

Definition df-or 360
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 21717). After we define the constant true  T. (df-tru 1328) and the constant false  F. (df-fal 1329), we will be able to prove these truth table values:  ( (  T.  \/  T.  )  <->  T.  ) (truortru 1349), 
( (  T.  \/  F.  )  <->  T.  ) (truorfal 1350), 
( (  F.  \/  T.  )  <->  T.  ) (falortru 1351), and  ( (  F.  \/  F.  )  <->  F.  ) (falorfal 1352).

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 228. This is the justification for the definition, along with the fact that it introduces a new symbol  \/. Contrast with  /\ (df-an 361), 
-> (wi 4),  -/\ (df-nan 1297), and  \/_ (df-xor 1314) . (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 358 . 2  wff  ( ph  \/  ps )
41wn 3 . . 3  wff  -.  ph
54, 2wi 4 . 2  wff  ( -. 
ph  ->  ps )
63, 5wb 177 1  wff  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
Colors of variables: wff set class
This definition is referenced by:  pm4.64  362  pm2.53  363  pm2.54  364  ori  365  orri  366  ord  367  imor  402  mtord  642  orbi2d  683  orimdi  821  ordi  835  pm5.17  859  pm5.6  879  orbidi  899  cador  1400  cadan  1401  19.30  1614  19.43  1615  nfor  1858  19.32  1896  dfsb3  2116  sbor  2140  neor  2682  r19.30  2845  r19.32v  2846  r19.43  2855  dfif2  3733  disjor  4188  sotric  4521  sotrieq  4522  isso2i  4527  soxp  6450  unxpwdom2  7545  cflim2  8132  cfpwsdom  8448  ltapr  8911  ltxrlt  9135  isprm4  13077  euclemma  13096  islpi  17201  restntr  17234  alexsubALTlem2  18067  alexsubALTlem3  18068  2bornot2b  21746  disjorf  24009  funcnv5mpt  24072  ballotlemodife  24743  3orit  25157  dfon2lem5  25398  ecase13d  26253  elicc3  26257  nn0prpw  26263  pm10.541  27477  r19.32  27859  sborNEW7  29418  dfsb3NEW7  29488
  Copyright terms: Public domain W3C validator