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

Definition df-an 360
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 1310) and the constant false  F. (df-fal 1311), we will be able to prove these truth table values:  ( (  T.  /\  T.  )  <->  T.  ) (truantru 1326), 
( (  T.  /\  F.  )  <->  F.  ) (truanfal 1327),  ( (  F.  /\  T.  )  <->  F.  ) (falantru 1328), and  ( (  F.  /\  F.  )  <->  F.  ) (falanfal 1329).

Contrast with  \/ (df-or 359), 
-> (wi 4),  -/\ (df-nan 1288), and  \/_ (df-xor 1296) . (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 358 . 2  wff  ( ph  /\ 
ps )
42wn 3 . . . 4  wff  -.  ps
51, 4wi 4 . . 3  wff  ( ph  ->  -.  ps )
65wn 3 . 2  wff  -.  ( ph  ->  -.  ps )
73, 6wb 176 1  wff  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
Colors of variables: wff set class
This definition is referenced by:  pm4.63  410  imnan  411  imp  418  ex  423  pm4.54  479  dfbi2  609  pm5.32  617  hban  1748  nfand  1775  nfan  1783  equsex  1915  sban  2022  r19.35  2700  dfac5lem4  7769  kmlem3  7794  axrepprim  24063  axunprim  24064  axregprim  24066  axinfprim  24067  axacprim  24068  pm11.52  27688  equsexNEW7  29467  sbanNEW7  29544  equsexv-x12  29735  ax9lem10  29771
  Copyright terms: Public domain W3C validator