MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-an Structured version   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 1329) and the constant false  F. (df-fal 1330), we will be able to prove these truth table values:  ( (  T.  /\  T.  )  <->  T.  ) (truantru 1346), 
( (  T.  /\  F.  )  <->  F.  ) (truanfal 1347),  ( (  F.  /\  T.  )  <->  F.  ) (falantru 1348), and  ( (  F.  /\  F.  )  <->  F.  ) (falanfal 1349).

Contrast with  \/ (df-or 361), 
-> (wi 4),  -/\ (df-nan 1298), and  \/_ (df-xor 1315) . (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 3 . . . 4  wff  -.  ps
51, 4wi 4 . . 3  wff  ( ph  ->  -.  ps )
65wn 3 . 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  nfand  1846  nfanOLD  1851  hbanOLD  1854  equsexOLD  2007  sban  2145  r19.35  2862  dfac5lem4  8045  kmlem3  8070  axrepprim  25186  axunprim  25187  axregprim  25189  axinfprim  25190  axacprim  25191  pm11.52  27674  equsexNEW7  29664  sbanNEW7  29743
  Copyright terms: Public domain W3C validator