MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-or Structured version   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 21731). After we define the constant true  T. (df-tru 1329) and the constant false  F. (df-fal 1330), we will be able to prove these truth table values:  ( (  T.  \/  T.  )  <->  T.  ) (truortru 1350), 
( (  T.  \/  F.  )  <->  T.  ) (truorfal 1351), 
( (  F.  \/  T.  )  <->  T.  ) (falortru 1352), and  ( (  F.  \/  F.  )  <->  F.  ) (falorfal 1353).

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 4),  -/\ (df-nan 1298), and  \/_ (df-xor 1315) . (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 3 . . 3  wff  -.  ph
54, 2wi 4 . 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  1401  cadan  1402  19.30  1615  19.43  1616  nfor  1859  19.32  1897  dfsb3  2111  sbor  2140  neor  2690  r19.30  2855  r19.32v  2856  r19.43  2865  dfif2  3743  disjor  4198  sotric  4531  sotrieq  4532  isso2i  4537  soxp  6461  unxpwdom2  7558  cflim2  8145  cfpwsdom  8461  ltapr  8924  ltxrlt  9148  isprm4  13091  euclemma  13110  islpi  17215  restntr  17248  alexsubALTlem2  18081  alexsubALTlem3  18082  2bornot2b  21760  disjorf  24023  funcnv5mpt  24086  ballotlemodife  24757  3orit  25171  dfon2lem5  25416  ecase13d  26318  elicc3  26322  nn0prpw  26328  pm10.541  27541  r19.32  27923  sborNEW7  29628  dfsb3NEW7  29701
  Copyright terms: Public domain W3C validator