HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-an 225
Description: Define conjunction (logical 'and'). Definition of [Margaris] p. 49.
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 223 . 2 wff (ph /\ ps)
42wn 2 . . . 4 wff -. ps
51, 4wi 3 . . 3 wff (ph -> -. ps)
65wn 2 . 2 wff -. (ph -> -. ps)
73, 6wb 146 1 wff ((ph /\ ps) <-> -. (ph -> -. ps))
Colors of variables: wff set class
This definition is referenced by:  pm4.63 228  iman 237  imnan 242  pm3.2 283  jca 288  anor 304  pm3.26 319  pm3.27 323  impexp 347  anass 439  bi 513  pm5.32 642  hban 1006  19.29 1067  19.35 1071  equsex 1148  sban 1232  r19.35 1751  aceq5lem4 4710  kmlem3 4739  nmcopexlem1 9866  nmcfnexlem1 9895
Copyright terms: Public domain