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  2122  r19.35  2819  dfac5lem4  7967  kmlem3  7992  axrepprim  25108  axunprim  25109  axregprim  25111  axinfprim  25112  axacprim  25113  pm11.52  27457  equsexNEW7  29200  sbanNEW7  29277
  Copyright terms: Public domain W3C validator