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

Definition df-an 361
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 1325) and the constant false  F. (df-fal 1326), we will be able to prove these truth table values:  ( (  T.  /\  T.  )  <->  T.  ) (truantru 1342), 
( (  T.  /\  F.  )  <->  F.  ) (truanfal 1343),  ( (  F.  /\  T.  )  <->  F.  ) (falantru 1344), and  ( (  F.  /\  F.  )  <->  F.  ) (falanfal 1345).

Contrast with  \/ (df-or 360), 
-> (wi 4),  -/\ (df-nan 1294), and  \/_ (df-xor 1311) . (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 359 . 2  wff  ( ph  /\ 
ps )
42wn 3 . . . 4  wff  -.  ps
51, 4wi 4 . . 3  wff  ( ph  ->  -.  ps )
65wn 3 . 2  wff  -.  ( ph  ->  -.  ps )
73, 6wb 177 1  wff  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
Colors of variables: wff set class
This definition is referenced by:  pm4.63  411  imnan  412  imp  419  ex  424  pm4.54  480  dfbi2  610  pm5.32  618  nfand  1833  nfanOLD  1838  hbanOLD  1841  equsexOLD  1960  sban  2103  r19.35  2799  dfac5lem4  7941  kmlem3  7966  axrepprim  24931  axunprim  24932  axregprim  24934  axinfprim  24935  axacprim  24936  pm11.52  27255  equsexNEW7  28829  sbanNEW7  28906
  Copyright terms: Public domain W3C validator