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  1839  nfanOLD  1844  hbanOLD  1847  equsexOLD  1970  sban  2118  r19.35  2815  dfac5lem4  7963  kmlem3  7988  axrepprim  25104  axunprim  25105  axregprim  25107  axinfprim  25108  axacprim  25109  pm11.52  27453  equsexNEW7  29196  sbanNEW7  29273
  Copyright terms: Public domain W3C validator