MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-or Structured version   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 21729). 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  2109  sbor  2138  neor  2688  r19.30  2853  r19.32v  2854  r19.43  2863  dfif2  3741  disjor  4196  sotric  4529  sotrieq  4530  isso2i  4535  soxp  6459  unxpwdom2  7556  cflim2  8143  cfpwsdom  8459  ltapr  8922  ltxrlt  9146  isprm4  13089  euclemma  13108  islpi  17213  restntr  17246  alexsubALTlem2  18079  alexsubALTlem3  18080  2bornot2b  21758  disjorf  24021  funcnv5mpt  24084  ballotlemodife  24755  3orit  25169  dfon2lem5  25414  ecase13d  26316  elicc3  26320  nn0prpw  26326  pm10.541  27539  r19.32  27921  sborNEW7  29566  dfsb3NEW7  29639
  Copyright terms: Public domain W3C validator