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

Definition df-an 362
Description: Define conjunction (logical 'and'). Definition of [Margaris] p. 49. When both the left and right operand are true, the result is true; when either is false, the result is false. For example, it is true that  ( 2  =  2  /\  3  =  3 ). After we define the constant true  T. (df-tru 1312) and the constant false  F. (df-fal 1313), we will be able to prove these truth table values:  ( (  T.  /\  T.  )  <->  T.  ) (truantru 1328), 
( (  T.  /\  F.  )  <->  F.  ) (truanfal 1329),  ( (  F.  /\  T.  )  <->  F.  ) (falantru 1330), and  ( (  F.  /\  F.  )  <->  F.  ) (falanfal 1331).

Contrast with  \/ (df-or 361), 
-> (wi 6),  -/\ (df-nan 1290), and  \/_ (df-xor 1298) . (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
df-an  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wa 360 . 2  wff  ( ph  /\ 
ps )
42wn 5 . . . 4  wff  -.  ps
51, 4wi 6 . . 3  wff  ( ph  ->  -.  ps )
65wn 5 . 2  wff  -.  ( ph  ->  -.  ps )
73, 6wb 178 1  wff  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
Colors of variables: wff set class
This definition is referenced by:  pm4.63  412  imnan  413  imp  420  ex  425  pm4.54  481  dfbi2  611  pm5.32  619  hban  1740  nfand  1767  nfan  1775  equsex  1907  sban  2010  r19.35  2690  dfac5lem4  7750  kmlem3  7775  axrepprim  23454  axunprim  23455  axregprim  23457  axinfprim  23458  axacprim  23459  pm11.52  26986  equsexv-x12  28382  ax9lem10  28418
  Copyright terms: Public domain W3C validator